NF weak partition development: Flypitch4.LanguageExtension.

Language.Lconstants, Language.sum, Language.symbols

def NFChoice.Fol.Language.Lconstants (α : Type u) : Language

Flypitch construction Lconstants, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.Language.Lconstants α = { functions := fun (n : ℕ) => Nat.rec α (fun (_n : ℕ) (_ih : Type ?u.1) => PEmpty.{?u.1 + 1}) n, relations := fun (_n : ℕ) => PEmpty.{?u.1 + 1} }

def NFChoice.Fol.Language.sum (L L' : Language) : Language

Flypitch construction sum, retained by the first-order soundness and completeness development.

Equations

• L.sum L' = { functions := fun (n : ℕ) => L.functions n ⊕ L'.functions n, relations := fun (n : ℕ) => L.relations n ⊕ L'.relations n }

def NFChoice.Fol.Language.symbols (L : Language) : Type u

Flypitch construction symbols, retained by the first-order soundness and completeness development.

Equations

• L.symbols = ((l : ℕ) × L.functions l ⊕ (l : ℕ) × L.relations l)

symbols_in_term, symbols_in_formula

def NFChoice.Fol.symbolsInTerm {L : Language} {l : ℕ} : preterm L l → Set L.symbols

Flypitch construction symbols_in_term, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.symbolsInTerm &_k = ∅
• NFChoice.Fol.symbolsInTerm (NFChoice.Fol.preterm.func f) = {Sum.inl ⟨x✝, f⟩}
• NFChoice.Fol.symbolsInTerm (t₁.app t₂) = NFChoice.Fol.symbolsInTerm t₁ ∪ NFChoice.Fol.symbolsInTerm t₂

def NFChoice.Fol.symbolsInFormula {L : Language} {l : ℕ} : preformula l → Set L.symbols

Flypitch construction symbols_in_formula, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.symbolsInFormula ⊥' = ∅
• NFChoice.Fol.symbolsInFormula (NFChoice.Fol.preformula.equal t₁ t₂) = NFChoice.Fol.symbolsInTerm t₁ ∪ NFChoice.Fol.symbolsInTerm t₂
• NFChoice.Fol.symbolsInFormula (NFChoice.Fol.preformula.rel R) = {Sum.inr ⟨x✝, R⟩}
• NFChoice.Fol.symbolsInFormula (f.apprel t) = NFChoice.Fol.symbolsInFormula f ∪ NFChoice.Fol.symbolsInTerm t
• NFChoice.Fol.symbolsInFormula (f₁.imp f₂) = NFChoice.Fol.symbolsInFormula f₁ ∪ NFChoice.Fol.symbolsInFormula f₂
• NFChoice.Fol.symbolsInFormula f.all = NFChoice.Fol.symbolsInFormula f

@[simp]

theorem NFChoice.Fol.symbols_in_term_lift_at {L : Language} (n m : ℕ) {l : ℕ} (t : preterm L l) : symbolsInTerm (t ↑' n # m) = symbolsInTerm t

theorem NFChoice.Fol.symbols_in_term_lift {L : Language} (n : ℕ) {l : ℕ} (t : preterm L l) : symbolsInTerm (t ↑ n) = symbolsInTerm t

theorem NFChoice.Fol.symbols_in_term_subst {L : Language} (s : term L) (n : ℕ) {l : ℕ} (t : preterm L l) : symbolsInTerm (substTerm t s n) ⊆ symbolsInTerm t ∪ symbolsInTerm s

theorem NFChoice.Fol.symbols_in_formula_subst {L : Language} {l : ℕ} (f : preformula l) (s : term L) (n : ℕ) : symbolsInFormula (f [s // n]f) ⊆ symbolsInFormula f ∪ symbolsInTerm s

Lhom — language homomorphism

structure NFChoice.Fol.Lhom (L L' : Language) : Type u

Flypitch construction Lhom, retained by the first-order soundness and completeness development.

• onFunction {n : ℕ} : L.functions n → L'.functions n

  The on_function component of the corresponding first-order structure.

• onRelation {n : ℕ} : L.relations n → L'.relations n

  The on_relation component of the corresponding first-order structure.

def NFChoice.Fol.«term_→ᴸ_» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

• NFChoice.Fol.«term_→ᴸ_» = Lean.ParserDescr.trailingNode `NFChoice.Fol.«term_→ᴸ_» 10 11 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →ᴸ ") (Lean.ParserDescr.cat `term 11))

def NFChoice.Fol.Lhom.id (L : Language) : L →ᴸ L

Flypitch construction id, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.Lhom.id L = { onFunction := fun {x : ℕ} => id, onRelation := fun {x : ℕ} => id }

def NFChoice.Fol.Lhom.sumInl {L L' : Language} : L →ᴸ L.sum L'

Flypitch construction sum_inl, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.Lhom.sumInl = { onFunction := fun {x : ℕ} => Sum.inl, onRelation := fun {x : ℕ} => Sum.inl }

def NFChoice.Fol.Lhom.sumInr {L L' : Language} : L' →ᴸ L.sum L'

Flypitch construction sum_inr, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.Lhom.sumInr = { onFunction := fun {x : ℕ} => Sum.inr, onRelation := fun {x : ℕ} => Sum.inr }

@[reducible]

def NFChoice.Fol.Lhom.comp {L1 L2 L3 : Language} (g : L2 →ᴸ L3) (f : L1 →ᴸ L2) : L1 →ᴸ L3

Flypitch construction comp, retained by the first-order soundness and completeness development.

Equations

• g.comp f = { onFunction := fun {n : ℕ} => g.onFunction ∘ f.onFunction, onRelation := fun {n : ℕ} => g.onRelation ∘ f.onRelation }

theorem NFChoice.Fol.Lhom.Lhom_funext {L1 L2 : Language} {F G : L1 →ᴸ L2} (h_fun : @onFunction L1 L2 F = @onFunction L1 L2 G) (h_rel : @onRelation L1 L2 F = @onRelation L1 L2 G) : F = G

@[simp]

theorem NFChoice.Fol.Lhom.id_is_left_identity {L1 L2 : Language} {F : L1 →ᴸ L2} : (Lhom.id L2).comp F = F

@[simp]

theorem NFChoice.Fol.Lhom.id_is_right_identity {L1 L2 : Language} {F : L1 →ᴸ L2} : F.comp (Lhom.id L1) = F

structure NFChoice.Fol.Lhom.IsInjective {L L' : Language} (ϕ : L →ᴸ L') : Prop

Flypitch construction is_injective, retained by the first-order soundness and completeness development.

• onFunction {n : ℕ} : Function.Injective ϕ.onFunction
• onRelation {n : ℕ} : Function.Injective ϕ.onRelation

class NFChoice.Fol.Lhom.HasDecidableRange {L L' : Language} (ϕ : L →ᴸ L') : Type u

Flypitch construction has_decidable_range, retained by the first-order soundness and completeness development.

• onFunction {n : ℕ} : DecidablePred fun (x : L'.functions n) => x ∈ Set.range ϕ.onFunction

  The on_function component of the corresponding first-order structure.

• onRelation {n : ℕ} : DecidablePred fun (x : L'.relations n) => x ∈ Set.range ϕ.onRelation

  The on_relation component of the corresponding first-order structure.

@[instance_reducible, instance 100]

instance NFChoice.Fol.Lhom.instDecFn {L L' : Language} (ϕ : L →ᴸ L') [h : ϕ.HasDecidableRange] {n : ℕ} : DecidablePred fun (x : L'.functions n) => x ∈ Set.range ϕ.onFunction

Equations

• ϕ.instDecFn = NFChoice.Fol.Lhom.HasDecidableRange.onFunction

@[instance_reducible, instance 100]

instance NFChoice.Fol.Lhom.instDecRel {L L' : Language} (ϕ : L →ᴸ L') [h : ϕ.HasDecidableRange] {n : ℕ} : DecidablePred fun (x : L'.relations n) => x ∈ Set.range ϕ.onRelation

Equations

• ϕ.instDecRel = NFChoice.Fol.Lhom.HasDecidableRange.onRelation

def NFChoice.Fol.Lhom.onSymbol {L L' : Language} (ϕ : L →ᴸ L') : L.symbols → L'.symbols

Flypitch construction on_symbol, retained by the first-order soundness and completeness development.

Equations

• ϕ.onSymbol (Sum.inl ⟨l, f⟩) = Sum.inl ⟨l, ϕ.onFunction f⟩
• ϕ.onSymbol (Sum.inr ⟨l, R⟩) = Sum.inr ⟨l, ϕ.onRelation R⟩

def NFChoice.Fol.Lhom.onTerm {L L' : Language} (ϕ : L →ᴸ L') {l : ℕ} : preterm L l → preterm L' l

Flypitch construction on_term, retained by the first-order soundness and completeness development.

Equations

• ϕ.onTerm &_k = &_k
• ϕ.onTerm (NFChoice.Fol.preterm.func f) = NFChoice.Fol.preterm.func (ϕ.onFunction f)
• ϕ.onTerm (t₁.app t₂) = (ϕ.onTerm t₁).app (ϕ.onTerm t₂)

@[simp]

theorem NFChoice.Fol.Lhom.on_term_lift_at {L L' : Language} (ϕ : L →ᴸ L') {l : ℕ} (t : preterm L l) (n m : ℕ) : ϕ.onTerm (t ↑' n # m) = ϕ.onTerm t ↑' n # m

theorem NFChoice.Fol.Lhom.on_term_lift {L L' : Language} (ϕ : L →ᴸ L') {l : ℕ} (n : ℕ) (t : preterm L l) : ϕ.onTerm (t ↑ n) = ϕ.onTerm t ↑ n

@[simp]

theorem NFChoice.Fol.Lhom.on_term_subst {L L' : Language} (ϕ : L →ᴸ L') {l : ℕ} (t : preterm L l) (s : term L) (n : ℕ) : ϕ.onTerm (substTerm t s n) = substTerm (ϕ.onTerm t) (ϕ.onTerm s) n

@[simp]

theorem NFChoice.Fol.Lhom.on_term_apps {L L' : Language} (ϕ : L →ᴸ L') {l : ℕ} (t : preterm L l) (ts : DVec (term L) l) : ϕ.onTerm (apps t ts) = apps (ϕ.onTerm t) (DVec.map ϕ.onTerm ts)

theorem NFChoice.Fol.Lhom.not_mem_symbols_in_term_on_term {L L' : Language} (ϕ : L →ᴸ L') {s : L'.symbols} (hs : s ∉ Set.range ϕ.onSymbol) {l : ℕ} (t : preterm L l) : s ∉ symbolsInTerm (ϕ.onTerm t)

def NFChoice.Fol.Lhom.onFormula {L L' : Language} (ϕ : L →ᴸ L') {l : ℕ} : preformula l → preformula l

Flypitch construction on_formula, retained by the first-order soundness and completeness development.

Equations

• ϕ.onFormula ⊥' = ⊥'
• ϕ.onFormula (NFChoice.Fol.preformula.equal t₁ t₂) = NFChoice.Fol.preformula.equal (ϕ.onTerm t₁) (ϕ.onTerm t₂)
• ϕ.onFormula (NFChoice.Fol.preformula.rel R) = NFChoice.Fol.preformula.rel (ϕ.onRelation R)
• ϕ.onFormula (f.apprel t) = (ϕ.onFormula f).apprel (ϕ.onTerm t)
• ϕ.onFormula (f₁.imp f₂) = (ϕ.onFormula f₁).imp (ϕ.onFormula f₂)
• ϕ.onFormula f.all = (ϕ.onFormula f).all

@[simp]

theorem NFChoice.Fol.Lhom.on_formula_lift_at {L L' : Language} (ϕ : L →ᴸ L') {l : ℕ} (n m : ℕ) (f : preformula l) : ϕ.onFormula (f ↑f' n # m) = ϕ.onFormula f ↑f' n # m

theorem NFChoice.Fol.Lhom.on_formula_lift {L L' : Language} (ϕ : L →ᴸ L') {l : ℕ} (n : ℕ) (f : preformula l) : ϕ.onFormula (f ↑f n) = ϕ.onFormula f ↑f n

@[simp]

theorem NFChoice.Fol.Lhom.on_formula_subst {L L' : Language} (ϕ : L →ᴸ L') {l : ℕ} (f : preformula l) (s : term L) (n : ℕ) : ϕ.onFormula (f [s // n]f) = ϕ.onFormula f [ϕ.onTerm s // n]f

@[simp]

theorem NFChoice.Fol.Lhom.on_formula_apps_rel {L L' : Language} (ϕ : L →ᴸ L') {l : ℕ} (f : preformula l) (ts : DVec (term L) l) : ϕ.onFormula (appsRel f ts) = appsRel (ϕ.onFormula f) (DVec.map ϕ.onTerm ts)

theorem NFChoice.Fol.Lhom.not_mem_symbols_in_formula_on_formula {L L' : Language} (ϕ : L →ᴸ L') {s : L'.symbols} (hs : s ∉ Set.range ϕ.onSymbol) {l : ℕ} (f : preformula l) : s ∉ symbolsInFormula (ϕ.onFormula f)

theorem NFChoice.Fol.Lhom.not_mem_function_in_formula_on_formula {L L' : Language} (ϕ : L →ᴸ L') {l' : ℕ} {f' : L'.functions l'} (h : f' ∉ Set.range ϕ.onFunction) {l : ℕ} (f : preformula l) : Sum.inl ⟨l', f'⟩ ∉ symbolsInFormula (ϕ.onFormula f)

on_bounded_term, on_bounded_formula

def NFChoice.Fol.Lhom.onBoundedTerm {L L' : Language} (ϕ : L →ᴸ L') {n l : ℕ} (_t : BoundedPreterm L n l) : BoundedPreterm L' n l

Flypitch construction on_bounded_term, retained by the first-order soundness and completeness development.

Equations

• ϕ.onBoundedTerm (NFChoice.Fol.bd_var k) = NFChoice.Fol.bd_var k
• ϕ.onBoundedTerm (NFChoice.Fol.bd_func f) = NFChoice.Fol.bd_func (ϕ.onFunction f)
• ϕ.onBoundedTerm (t.bd_app s) = (ϕ.onBoundedTerm t).bd_app (ϕ.onBoundedTerm s)

@[simp]

theorem NFChoice.Fol.Lhom.on_bounded_term_fst {L L' : Language} (ϕ : L →ᴸ L') {n l : ℕ} (t : BoundedPreterm L n l) : (ϕ.onBoundedTerm t).fst = ϕ.onTerm t.fst

def NFChoice.Fol.Lhom.onBoundedFormula {L L' : Language} (ϕ : L →ᴸ L') {n l : ℕ} (_f : BoundedPreformula L n l) : BoundedPreformula L' n l

Flypitch construction on_bounded_formula, retained by the first-order soundness and completeness development.

Equations

• ϕ.onBoundedFormula NFChoice.Fol.bd_falsum = NFChoice.Fol.bd_falsum
• ϕ.onBoundedFormula (NFChoice.Fol.bd_equal t₁ t₂) = NFChoice.Fol.bd_equal (ϕ.onBoundedTerm t₁) (ϕ.onBoundedTerm t₂)
• ϕ.onBoundedFormula (NFChoice.Fol.bd_rel R) = NFChoice.Fol.bd_rel (ϕ.onRelation R)
• ϕ.onBoundedFormula (f.bd_apprel t) = (ϕ.onBoundedFormula f).bd_apprel (ϕ.onBoundedTerm t)
• ϕ.onBoundedFormula (f₁.bd_imp f₂) = (ϕ.onBoundedFormula f₁).bd_imp (ϕ.onBoundedFormula f₂)
• ϕ.onBoundedFormula f.bd_all = (ϕ.onBoundedFormula f).bd_all

@[simp]

theorem NFChoice.Fol.Lhom.on_bounded_formula_fst {L L' : Language} (ϕ : L →ᴸ L') {n l : ℕ} (f : BoundedPreformula L n l) : (ϕ.onBoundedFormula f).fst = ϕ.onFormula f.fst

Functoriality lemmas

@[simp]

theorem NFChoice.Fol.Lhom.comp_on_term {L1 L2 L3 : Language} {l : ℕ} (g : L2 →ᴸ L3) (f : L1 →ᴸ L2) : (g.comp f).onTerm = g.onTerm ∘ f.onTerm

@[simp]

theorem NFChoice.Fol.Lhom.comp_on_formula {L1 L2 L3 : Language} {l : ℕ} (g : L2 →ᴸ L3) (f : L1 →ᴸ L2) : (g.comp f).onFormula = g.onFormula ∘ f.onFormula

@[simp]

theorem NFChoice.Fol.Lhom.comp_on_bounded_term {L1 L2 L3 : Language} {n l : ℕ} (g : L2 →ᴸ L3) (f : L1 →ᴸ L2) : (g.comp f).onBoundedTerm = g.onBoundedTerm ∘ f.onBoundedTerm

@[simp]

theorem NFChoice.Fol.Lhom.comp_on_bounded_formula {L1 L2 L3 : Language} {n l : ℕ} (g : L2 →ᴸ L3) (f : L1 →ᴸ L2) : (g.comp f).onBoundedFormula = g.onBoundedFormula ∘ f.onBoundedFormula

theorem NFChoice.Fol.Lhom.id_term {L : Language} {l : ℕ} (t : preterm L l) : (Lhom.id L).onTerm t = t

theorem NFChoice.Fol.Lhom.id_formula {L : Language} {l : ℕ} (f : preformula l) : (Lhom.id L).onFormula f = f

theorem NFChoice.Fol.Lhom.id_bounded_term {L : Language} {n l : ℕ} (t : BoundedPreterm L n l) : (Lhom.id L).onBoundedTerm t = t

theorem NFChoice.Fol.Lhom.id_bounded_formula {L : Language} {n l : ℕ} (f : BoundedPreformula L n l) : (Lhom.id L).onBoundedFormula f = f

def NFChoice.Fol.Lhom.onClosedTerm {L L' : Language} (ϕ : L →ᴸ L') (t : closedTerm L) : closedTerm L'

Flypitch construction on_closed_term, retained by the first-order soundness and completeness development.

Equations

• ϕ.onClosedTerm t = ϕ.onBoundedTerm t

def NFChoice.Fol.Lhom.onSentence {L L' : Language} (ϕ : L →ᴸ L') (f : sentence L) : sentence L'

Flypitch construction on_sentence, retained by the first-order soundness and completeness development.

Equations

• ϕ.onSentence f = ϕ.onBoundedFormula f

theorem NFChoice.Fol.Lhom.on_sentence_fst {L L' : Language} (ϕ : L →ᴸ L') (f : sentence L) : BoundedPreformula.fst (ϕ.onSentence f) = ϕ.onFormula (BoundedPreformula.fst f)

on_prf — Lhom lifts proofs

noncomputable def NFChoice.Fol.Lhom.onPrf {L L' : Language} (ϕ : L →ᴸ L') {Γ : Set (formula L)} {f : formula L} (h : prf Γ f) : prf (ϕ.onFormula '' Γ) (ϕ.onFormula f)

Flypitch construction on_prf, retained by the first-order soundness and completeness development.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NFChoice.Fol.Lhom.onSprf {L L' : Language} (ϕ : L →ᴸ L') {Γ : SentTheory L} {f : sentence L} (h : Γ.sprf f) : SentTheory.sprf (ϕ.onSentence '' Γ) (ϕ.onSentence f)

Flypitch construction on_sprf, retained by the first-order soundness and completeness development.

Equations

• ϕ.onSprf h = ⋯.mpr (⋯.mp (ϕ.onPrf h))

reflect_term

noncomputable def NFChoice.Fol.Lhom.reflectTerm {L L' : Language} (ϕ : L →ᴸ L') [ϕ.HasDecidableRange] (t : term L') (m : ℕ) : term L

Flypitch construction reflect_term, retained by the first-order soundness and completeness development.

Equations

• One or more equations did not get rendered due to their size.

theorem NFChoice.Fol.Lhom.reflect_term_apps_pos {L L' : Language} {ϕ : L →ᴸ L'} [ϕ.HasDecidableRange] {l : ℕ} {f : L'.functions l} (hf : f ∈ Set.range ϕ.onFunction) (ts : DVec (term L') l) (m : ℕ) : ϕ.reflectTerm (apps (preterm.func f) ts) m = apps (preterm.func (Classical.choose hf)) (DVec.map (fun (t : term L') => ϕ.reflectTerm t m) ts)

theorem NFChoice.Fol.Lhom.reflect_term_apps_neg {L L' : Language} {ϕ : L →ᴸ L'} [ϕ.HasDecidableRange] {l : ℕ} {f : L'.functions l} (hf : f ∉ Set.range ϕ.onFunction) (ts : DVec (term L') l) (m : ℕ) : ϕ.reflectTerm (apps (preterm.func f) ts) m = &m

theorem NFChoice.Fol.Lhom.reflect_term_const_pos {L L' : Language} {ϕ : L →ᴸ L'} [ϕ.HasDecidableRange] {c : L'.constants} (hf : c ∈ Set.range ϕ.onFunction) (m : ℕ) : ϕ.reflectTerm (preterm.func c) m = preterm.func (Classical.choose hf)

theorem NFChoice.Fol.Lhom.reflect_term_const_neg {L L' : Language} {ϕ : L →ᴸ L'} [ϕ.HasDecidableRange] {c : L'.constants} (hf : c ∉ Set.range ϕ.onFunction) (m : ℕ) : ϕ.reflectTerm (preterm.func c) m = &m

@[simp]

theorem NFChoice.Fol.Lhom.reflect_term_var {L L' : Language} {ϕ : L →ᴸ L'} [ϕ.HasDecidableRange] (k m : ℕ) : ϕ.reflectTerm (&k) m = &k ↑' 1 # m

@[simp]

theorem NFChoice.Fol.Lhom.reflect_term_on_term {L L' : Language} {ϕ : L →ᴸ L'} [ϕ.HasDecidableRange] (hϕ : ϕ.IsInjective) (t : term L) (m : ℕ) : ϕ.reflectTerm (ϕ.onTerm t) m = t ↑' 1 # m

theorem NFChoice.Fol.Lhom.reflect_term_lift_at {L L' : Language} {ϕ : L →ᴸ L'} [ϕ.HasDecidableRange] (_hϕ : ϕ.IsInjective) {n m m' : ℕ} (h : m ≤ m') (t : term L') : ϕ.reflectTerm (t ↑' n # m) (m' + n) = ϕ.reflectTerm t m' ↑' n # m

theorem NFChoice.Fol.Lhom.reflect_term_lift {L L' : Language} {ϕ : L →ᴸ L'} [ϕ.HasDecidableRange] (hϕ : ϕ.IsInjective) {n m : ℕ} (t : term L') : ϕ.reflectTerm (t ↑ n) (m + n) = ϕ.reflectTerm t m ↑ n

theorem NFChoice.Fol.Lhom.reflect_term_subst {L L' : Language} {ϕ : L →ᴸ L'} [ϕ.HasDecidableRange] (hϕ : ϕ.IsInjective) (n m : ℕ) (s t : term L') : ϕ.reflectTerm (substTerm t s n) (m + n) = substTerm (ϕ.reflectTerm t (m + n + 1)) (ϕ.reflectTerm s m) n

reflect_formula

noncomputable def NFChoice.Fol.Lhom.reflectFormulaAux' {L L' : Language} (ϕ : L →ᴸ L') [ϕ.HasDecidableRange] (f : formula L') : ℕ → formula L

Flypitch construction reflect_formula_aux', retained by the first-order soundness and completeness development.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NFChoice.Fol.Lhom.reflectFormula {L L' : Language} (ϕ : L →ᴸ L') [ϕ.HasDecidableRange] (m : ℕ) (f : formula L') : formula L

Flypitch construction reflect_formula, retained by the first-order soundness and completeness development.

Equations

• ϕ.reflectFormula m f = ϕ.reflectFormulaAux' f m

theorem NFChoice.Fol.Lhom.reflect_formula_apps_rel_pos {L L' : Language} {ϕ : L →ᴸ L'} [ϕ.HasDecidableRange] {l : ℕ} {R : L'.relations l} (hR : R ∈ Set.range ϕ.onRelation) (ts : DVec (term L') l) (m : ℕ) : ϕ.reflectFormula m (appsRel (preformula.rel R) ts) = appsRel (preformula.rel (Classical.choose hR)) (DVec.map (fun (t : term L') => ϕ.reflectTerm t m) ts)

theorem NFChoice.Fol.Lhom.reflect_formula_apps_rel_neg {L L' : Language} {ϕ : L →ᴸ L'} [ϕ.HasDecidableRange] {l : ℕ} {R : L'.relations l} (hR : R ∉ Set.range ϕ.onRelation) (ts : DVec (term L') l) (m : ℕ) : ϕ.reflectFormula m (appsRel (preformula.rel R) ts) = ⊥'

@[simp]

theorem NFChoice.Fol.Lhom.reflect_formula_equal {L L' : Language} {ϕ : L →ᴸ L'} [ϕ.HasDecidableRange] (t₁ t₂ : term L') (m : ℕ) : ϕ.reflectFormula m (preformula.equal t₁ t₂) = preformula.equal (ϕ.reflectTerm t₁ m) (ϕ.reflectTerm t₂ m)

@[simp]

theorem NFChoice.Fol.Lhom.reflect_formula_imp {L L' : Language} {ϕ : L →ᴸ L'} [ϕ.HasDecidableRange] (f₁ f₂ : formula L') (m : ℕ) : ϕ.reflectFormula m (preformula.imp f₁ f₂) = preformula.imp (ϕ.reflectFormula m f₁) (ϕ.reflectFormula m f₂)

@[simp]

theorem NFChoice.Fol.Lhom.reflect_formula_all {L L' : Language} {ϕ : L →ᴸ L'} [ϕ.HasDecidableRange] (f : formula L') (m : ℕ) : ϕ.reflectFormula m (preformula.all f) = preformula.all (ϕ.reflectFormula (m + 1) f)

@[simp]

theorem NFChoice.Fol.Lhom.reflect_formula_on_formula {L L' : Language} {ϕ : L →ᴸ L'} [ϕ.HasDecidableRange] (hϕ : ϕ.IsInjective) (m : ℕ) (f : formula L) : ϕ.reflectFormula m (ϕ.onFormula f) = f ↑f' 1 # m

theorem NFChoice.Fol.Lhom.reflect_formula_lift_at {L L' : Language} {ϕ : L →ᴸ L'} [ϕ.HasDecidableRange] (hϕ : ϕ.IsInjective) {n m m' : ℕ} (h : m ≤ m') (f : formula L') : ϕ.reflectFormula (m' + n) (f ↑f' n # m) = ϕ.reflectFormula m' f ↑f' n # m

theorem NFChoice.Fol.Lhom.reflect_formula_lift {L L' : Language} {ϕ : L →ᴸ L'} [ϕ.HasDecidableRange] (hϕ : ϕ.IsInjective) (n m : ℕ) (f : formula L') : ϕ.reflectFormula (m + n) (f ↑f n) = ϕ.reflectFormula m f ↑f n

theorem NFChoice.Fol.Lhom.reflect_formula_lift1 {L L' : Language} {ϕ : L →ᴸ L'} [ϕ.HasDecidableRange] (hϕ : ϕ.IsInjective) (m : ℕ) (f : formula L') : ϕ.reflectFormula (m + 1) (f ↑f 1) = ϕ.reflectFormula m f ↑f 1

theorem NFChoice.Fol.Lhom.reflect_formula_subst {L L' : Language} {ϕ : L →ᴸ L'} [ϕ.HasDecidableRange] (hϕ : ϕ.IsInjective) (f : formula L') (n m : ℕ) (s : term L') : ϕ.reflectFormula (m + n) (f [s // n]f) = ϕ.reflectFormula (m + n + 1) f [ϕ.reflectTerm s m // n]f

@[simp]

theorem NFChoice.Fol.Lhom.reflect_formula_subst0 {L L' : Language} {ϕ : L →ᴸ L'} [ϕ.HasDecidableRange] (hϕ : ϕ.IsInjective) (m : ℕ) (f : formula L') (s : term L') : ϕ.reflectFormula m (f [s // 0]f) = ϕ.reflectFormula (m + 1) f [ϕ.reflectTerm s m // 0]f

reflect_prf_gen

noncomputable def NFChoice.Fol.Lhom.reflectPrfGen {L L' : Language} {ϕ : L →ᴸ L'} [ϕ.HasDecidableRange] (hϕ : ϕ.IsInjective) {Γ : Set (formula L')} {f : formula L'} (m : ℕ) (H : prf Γ f) : prf ((fun (g : formula L') => ϕ.reflectFormula m g) '' Γ) (ϕ.reflectFormula m f)

Flypitch construction reflect_prf_gen, retained by the first-order soundness and completeness development.

Equations

• One or more equations did not get rendered due to their size.

filter_symbols

@[reducible]

def NFChoice.Fol.Lhom.filterSymbols {L : Language} (p : L.symbols → Prop) : Language

Flypitch construction filter_symbols, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.Lhom.filterSymbols p = { functions := fun (l : ℕ) => { f : L.functions l // p (Sum.inl ⟨l, f⟩) }, relations := fun (l : ℕ) => { R : L.relations l // p (Sum.inr ⟨l, R⟩) } }

def NFChoice.Fol.Lhom.filterSymbolsLhom {L : Language} (p : L.symbols → Prop) : filterSymbols p →ᴸ L

Flypitch construction filter_symbols_Lhom, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.Lhom.filterSymbolsLhom p = { onFunction := fun {x : ℕ} => Subtype.val, onRelation := fun {x : ℕ} => Subtype.val }

theorem NFChoice.Fol.Lhom.is_injective_filter_symbols_Lhom {L : Language} (p : L.symbols → Prop) : (filterSymbolsLhom p).IsInjective

noncomputable def NFChoice.Fol.Lhom.findTermFilterSymbols {L : Language} (p : L.symbols → Prop) {l : ℕ} (t : preterm L l) (_h : symbolsInTerm t ⊆ {s : L.symbols | p s}) : { t' : preterm (filterSymbols p) l // (filterSymbolsLhom p).onTerm t' = t }

Flypitch construction find_term_filter_symbols, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.Lhom.findTermFilterSymbols p (&k) _h = ⟨&k, ⋯⟩
• NFChoice.Fol.Lhom.findTermFilterSymbols p (NFChoice.Fol.preterm.func f) h = ⟨NFChoice.Fol.preterm.func ⟨f, ⋯⟩, ⋯⟩
• NFChoice.Fol.Lhom.findTermFilterSymbols p (t₁.app t₂) h = ⟨(↑(NFChoice.Fol.Lhom.findTermFilterSymbols p t₁ ⋯)).app ↑(NFChoice.Fol.Lhom.findTermFilterSymbols p t₂ ⋯), ⋯⟩

noncomputable def NFChoice.Fol.Lhom.findFormulaFilterSymbols {L : Language} (p : L.symbols → Prop) {l : ℕ} (f : preformula l) (_h : symbolsInFormula f ⊆ {s : L.symbols | p s}) : { f' : preformula l // (filterSymbolsLhom p).onFormula f' = f }

Flypitch construction find_formula_filter_symbols, retained by the first-order soundness and completeness development.

Equations

• One or more equations did not get rendered due to their size.
• NFChoice.Fol.Lhom.findFormulaFilterSymbols p ⊥' x_3 = ⟨⊥', ⋯⟩
• NFChoice.Fol.Lhom.findFormulaFilterSymbols p (NFChoice.Fol.preformula.rel R) h = ⟨NFChoice.Fol.preformula.rel ⟨R, ⋯⟩, ⋯⟩
• NFChoice.Fol.Lhom.findFormulaFilterSymbols p (f.apprel t) h = ⟨(↑(NFChoice.Fol.Lhom.findFormulaFilterSymbols p f ⋯)).apprel ↑(NFChoice.Fol.Lhom.findTermFilterSymbols p t ⋯), ⋯⟩
• NFChoice.Fol.Lhom.findFormulaFilterSymbols p (f₁.imp f₂) h = ⟨(↑(NFChoice.Fol.Lhom.findFormulaFilterSymbols p f₁ ⋯)).imp ↑(NFChoice.Fol.Lhom.findFormulaFilterSymbols p f₂ ⋯), ⋯⟩
• NFChoice.Fol.Lhom.findFormulaFilterSymbols p f.all h = ⟨(↑(NFChoice.Fol.Lhom.findFormulaFilterSymbols p f h)).all, ⋯⟩

generalize_constant

noncomputable def NFChoice.Fol.Lhom.generalizeConstant {L : Language} {Γ : Set (formula L)} (c : L.constants) (hΓ : Sum.inl ⟨0, c⟩ ∉ ⋃₀ (symbolsInFormula '' Γ)) {f : formula L} (hf : Sum.inl ⟨0, c⟩ ∉ symbolsInFormula f) (H : prf Γ (f [preterm.func c // 0]f)) : prf Γ (preformula.all f)

Flypitch construction generalize_constant, retained by the first-order soundness and completeness development.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NFChoice.Fol.Lhom.sgeneralizeConstant {L : Language} {T : SentTheory L} (c : L.constants) (hΓ : Sum.inl ⟨0, c⟩ ∉ ⋃₀ (symbolsInFormula '' T.fst)) {f : boundedFormula L 1} (hf : Sum.inl ⟨0, c⟩ ∉ symbolsInFormula (BoundedPreformula.fst f)) (H : T.sprf (subst0BoundedFormula f (bdConst c))) : T.sprf (bd_all f)

Flypitch construction sgeneralize_constant, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.Lhom.sgeneralizeConstant c hΓ hf H = id (NFChoice.Fol.Lhom.generalizeConstant c hΓ hf (⋯.mp H))

reflect_prf

noncomputable def NFChoice.Fol.Lhom.reflectPrf {L L' : Language} {ϕ : L →ᴸ L'} {Γ : Set (formula L)} {f : formula L} (hϕ : ϕ.IsInjective) (h : prf (ϕ.onFormula '' Γ) (ϕ.onFormula f)) : prf Γ f

Flypitch construction reflect_prf, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.Lhom.reflectPrf hϕ h = NFChoice.Fol.reflectPrfLift1 (have this := NFChoice.Fol.Lhom.reflectPrfGen hϕ 0 h; ⋯.mp this)

noncomputable def NFChoice.Fol.Lhom.reflectSprf {L L' : Language} {ϕ : L →ᴸ L'} {Γ : SentTheory L} {f : sentence L} (hϕ : ϕ.IsInjective) (h : SentTheory.sprf (ϕ.onSentence '' Γ) (ϕ.onSentence f)) : Γ.sprf f

Flypitch construction reflect_sprf, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.Lhom.reflectSprf hϕ h = NFChoice.Fol.Lhom.reflectPrf hϕ (⋯.mpr (⋯.mp h))

Injectivity of on_term / on_formula

theorem NFChoice.Fol.Lhom.on_term_inj {L L' : Language} {ϕ : L →ᴸ L'} (h : ϕ.IsInjective) {l : ℕ} : Function.Injective ϕ.onTerm

theorem NFChoice.Fol.Lhom.on_formula_inj {L L' : Language} {ϕ : L →ᴸ L'} (h : ϕ.IsInjective) {l : ℕ} : Function.Injective ϕ.onFormula

theorem NFChoice.Fol.Lhom.on_bounded_term_inj {L L' : Language} {ϕ : L →ᴸ L'} (h : ϕ.IsInjective) {n l : ℕ} : Function.Injective ϕ.onBoundedTerm

theorem NFChoice.Fol.Lhom.on_bounded_formula_inj {L L' : Language} {ϕ : L →ᴸ L'} (h : ϕ.IsInjective) {n l : ℕ} : Function.Injective ϕ.onBoundedFormula

reduct — L-structure from L'-structure via ϕ

def NFChoice.Fol.Lhom.reduct {L L' : Language} (ϕ : L →ᴸ L') (S : Structure L') : Structure L

Flypitch construction reduct, retained by the first-order soundness and completeness development.

Equations

• S[[ϕ]] = { carrier := S.carrier, funMap := fun {_n : ℕ} (f : L.functions _n) => S.funMap (ϕ.onFunction f), relMap := fun {_n : ℕ} (R : L.relations _n) => S.relMap (ϕ.onRelation R) }

def NFChoice.Fol.Lhom.«term_[[_]]» : Lean.TrailingParserDescr

Notation for the corresponding first-order syntax or interpretation operation.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NFChoice.Fol.Lhom.reduct_coe {L L' : Language} {ϕ : L →ᴸ L'} (S : Structure L') : S[[ϕ]].carrier = S.carrier

def NFChoice.Fol.Lhom.reductId {L L' : Language} {ϕ : L →ᴸ L'} {S : Structure L'} : S.carrier → S[[ϕ]].carrier

Flypitch construction reduct_id, retained by the first-order soundness and completeness development.

Equations

• NFChoice.Fol.Lhom.reductId = id

@[simp]

theorem NFChoice.Fol.Lhom.reduct_term_eq {L L' : Language} {ϕ : L →ᴸ L'} {S : Structure L'} (hϕ : ϕ.IsInjective) {n : ℕ} (xs : DVec S.carrier n) {l : ℕ} (t : BoundedPreterm L n l) (xs' : DVec S.carrier l) : realizeBoundedTerm xs (ϕ.onBoundedTerm t) xs' = realizeBoundedTerm xs t xs'

theorem NFChoice.Fol.Lhom.reduct_bounded_formula_iff {L L' : Language} {ϕ : L →ᴸ L'} {S : Structure L'} (hϕ : ϕ.IsInjective) {n l : ℕ} (xs : DVec S.carrier n) (xs' : DVec S.carrier l) (f : BoundedPreformula L n l) : realizeBoundedFormula xs (ϕ.onBoundedFormula f) xs' ↔ realizeBoundedFormula xs f xs'

theorem NFChoice.Fol.Lhom.reduct_ssatisfied {L L' : Language} {ϕ : L →ᴸ L'} {S : Structure L'} {f : sentence L} (hϕ : ϕ.IsInjective) (h : realizeSentence S (ϕ.onSentence f)) : realizeSentence (S[[ϕ]]) f

theorem NFChoice.Fol.Lhom.reduct_ssatisfied' {L L' : Language} {ϕ : L →ᴸ L'} {S : Structure L'} {f : sentence L} (hϕ : ϕ.IsInjective) (h : realizeSentence S (ϕ.onBoundedFormula f)) : realizeSentence (S[[ϕ]]) f

theorem NFChoice.Fol.Lhom.reduct_all_ssatisfied {L L' : Language} {ϕ : L →ᴸ L'} {S : Structure L'} {T : SentTheory L} (hϕ : ϕ.IsInjective) (h : allRealizeSentence S (ϕ.onSentence '' T)) : allRealizeSentence (S[[ϕ]]) T

theorem NFChoice.Fol.Lhom.reduct_nonempty_of_nonempty {L L' : Language} {ϕ : L →ᴸ L'} {S : Structure L'} (H : Nonempty S.carrier) : Nonempty S[[ϕ]].carrier

@[reducible]

def NFChoice.Fol.Lhom.TheoryInduced {L L' : Language} (ϕ : L →ᴸ L') (T : SentTheory L) : SentTheory L'

Flypitch construction Theory_induced, retained by the first-order soundness and completeness development.

Equations

• ϕ.TheoryInduced T = ϕ.onSentence '' T

theorem NFChoice.Fol.Lhom.is_consistent_Theory_induced {L L' : Language} {ϕ : L →ᴸ L'} (hϕ : ϕ.IsInjective) {T : SentTheory L} (hT : T.isConsistent) : (ϕ.TheoryInduced T).isConsistent

is_consistent_extend (the main compactness argument)

theorem NFChoice.Fol.Lhom.is_consistent_finite_witness_extension {L L' : Language} {ϕ : L →ᴸ L'} {T : SentTheory L} (hT : T.isConsistent) (hϕ : ϕ.IsInjective) (h : boundedFormula L 1 → boundedFormula L 1) (hT' : ∀ (f : boundedFormula L 1), T.sprovable (bdEx (h f))) (g : boundedFormula L 1 → L'.constants) (hg : Function.Injective g) (hg' : ∀ (x : boundedFormula L 1), g x ∉ Set.range ϕ.onFunction) (s₀ : Finset (boundedFormula L 1)) : (ϕ.TheoryInduced T ∪ (fun (f : boundedFormula L 1) => subst0BoundedFormula (ϕ.onBoundedFormula (h f)) (bdConst (g f))) '' ↑s₀).isConsistent

theorem NFChoice.Fol.Lhom.is_consistent_extend {L L' : Language} {ϕ : L →ᴸ L'} {T : SentTheory L} (hT : T.isConsistent) (hϕ : ϕ.IsInjective) (h : boundedFormula L 1 → boundedFormula L 1) (hT' : ∀ (f : boundedFormula L 1), T.sprovable (bdEx (h f))) (g : boundedFormula L 1 → L'.constants) (hg : Function.Injective g) (hg' : ∀ (x : boundedFormula L 1), g x ∉ Set.range ϕ.onFunction) : (ϕ.TheoryInduced T ∪ (fun (f : boundedFormula L 1) => subst0BoundedFormula (ϕ.onBoundedFormula (h f)) (bdConst (g f))) '' Set.univ).isConsistent