NF weak partition development: Flypitch4.Henkin.

Directed colimits of languages

These are fieldwise (and then indexwise) colimits of types. For the Henkin construction, the directed type is always ℕ' (carrier = ℕ : Type 0), so we can use a single universe u for the language symbols.

structure NFChoice.Fol.DirectedDiagramLanguage : Type (u + 1)

A directed diagram of Languages at universe u indexed by ℕ

• obj : ℕ → Language

  The obj component of the corresponding first-order structure.

• mor {x y : ℕ} : x ≤ y → (self.obj x →ᴸ self.obj y)

  The mor component of the corresponding first-order structure.

• h_mor {x y z : ℕ} {f1 : x ≤ y} {f2 : y ≤ z} {f3 : x ≤ z} : self.mor f3 = (self.mor f2).comp (self.mor f1)

def NFChoice.Fol.diagramFunctions (F : DirectedDiagramLanguage) (n : ℕ) : colimit.DirectedDiagram ℕ'

Restrict to n-ary function family

Equations

• NFChoice.Fol.diagramFunctions F n = { obj := fun (x : ℕ'.carrier) => (F.obj x).functions n, mor := fun {x y : ℕ'.carrier} (h : ℕ'.rel x y) => (F.mor h).onFunction, h_mor := ⋯ }

def NFChoice.Fol.diagramRelations (F : DirectedDiagramLanguage) (n : ℕ) : colimit.DirectedDiagram ℕ'

Restrict to n-ary relation family

Equations

• NFChoice.Fol.diagramRelations F n = { obj := fun (x : ℕ'.carrier) => (F.obj x).relations n, mor := fun {x y : ℕ'.carrier} (h : ℕ'.rel x y) => (F.mor h).onRelation, h_mor := ⋯ }

def NFChoice.Fol.colimitLanguage (F : DirectedDiagramLanguage) : Language

The colimit language

Equations

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

def NFChoice.Fol.canonicalMapLanguage {F : DirectedDiagramLanguage} (i : ℕ) : F.obj i →ᴸ colimitLanguage F

Canonical map from stage i into the colimit language

Equations

• NFChoice.Fol.canonicalMapLanguage i = { onFunction := fun {n : ℕ} => NFChoice.colimit.canonicalMap i, onRelation := fun {n : ℕ} => NFChoice.colimit.canonicalMap i }

structure NFChoice.Fol.CoconeLanguage (F : DirectedDiagramLanguage) : Type (u + 1)

A cocone over a directed diagram of languages

• vertex : Language

  The vertex component of the corresponding first-order structure.

• map (i : ℕ) : F.obj i →ᴸ self.vertex

  The map component of the corresponding first-order structure.

• h_compat {i j : ℕ} (h : i ≤ j) : self.map i = (self.map j).comp (F.mor h)

def NFChoice.Fol.coconeOfColimitLanguage (F : DirectedDiagramLanguage) : CoconeLanguage F

The colimit is itself a cocone

Equations

• NFChoice.Fol.coconeOfColimitLanguage F = { vertex := NFChoice.Fol.colimitLanguage F, map := NFChoice.Fol.canonicalMapLanguage, h_compat := ⋯ }

The Henkin construction

inductive NFChoice.Fol.HenkinLanguageFunctions (L : Language) : ℕ → Type u

Inductive type of function symbols for one Henkin step. inc embeds L-symbols; wit introduces witness constants.

• inc {L : Language} {n : ℕ} : L.functions n → HenkinLanguageFunctions L n
• wit {L : Language} : boundedFormula L 1 → HenkinLanguageFunctions L 0

@[reducible]

def NFChoice.Fol.henkinLanguageStep (L : Language) : Language

One Henkin step on languages

Equations

• NFChoice.Fol.henkinLanguageStep L = { functions := NFChoice.Fol.HenkinLanguageFunctions L, relations := L.relations }

def NFChoice.Fol.wit' {L : Language} : boundedFormula L 1 → (henkinLanguageStep L).constants

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

Equations

• NFChoice.Fol.wit' = NFChoice.Fol.HenkinLanguageFunctions.wit

def NFChoice.Fol.henkinLanguageInclusion {L : Language} : L →ᴸ henkinLanguageStep L

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

Equations

• NFChoice.Fol.henkinLanguageInclusion = { onFunction := fun {x : ℕ} (f : L.functions x) => NFChoice.Fol.HenkinLanguageFunctions.inc f, onRelation := fun {x : ℕ} => id }

theorem NFChoice.Fol.henkin_language_inclusion_inj {L : Language} : henkinLanguageInclusion.IsInjective

wit_property and henkin_theory_step

@[reducible]

def NFChoice.Fol.witProperty {L : Language} (f : boundedFormula L 1) (c : L.constants) : sentence L

The witnessing sentence: (∃ᵇf) → f[c/0]

Equations

• NFChoice.Fol.witProperty f c = NFChoice.Fol.bd_imp (NFChoice.Fol.bdEx f) (NFChoice.Fol.subst0BoundedFormula f (NFChoice.Fol.bdConst c))

def NFChoice.Fol.henkinTheoryStep {L : Language} (T : SentTheory L) : SentTheory (henkinLanguageStep L)

One Henkin step on theories

Equations

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

theorem NFChoice.Fol.is_consistent_henkin_theory_step {L : Language} {T : SentTheory L} (hT : T.isConsistent) : (henkinTheoryStep T).isConsistent

The Henkin extension of a consistent theory is consistent

Henkin language chain

@[reducible]

def NFChoice.Fol.henkinLanguageChainObjects {L : Language} : ℕ → Language

Objects of the Henkin language chain

Equations

• NFChoice.Fol.henkinLanguageChainObjects 0 = L
• NFChoice.Fol.henkinLanguageChainObjects n.succ = NFChoice.Fol.henkinLanguageStep (NFChoice.Fol.henkinLanguageChainObjects n)

theorem NFChoice.Fol.obvious {L : Language} (i : ℕ) : HenkinLanguageFunctions (henkinLanguageChainObjects i) 0 = (henkinLanguageChainObjects (i + 1)).constants

def NFChoice.Fol.henkinLanguageChainMaps (L : Language) (x y : ℕ) : x ≤ y → (henkinLanguageChainObjects x →ᴸ henkinLanguageChainObjects y)

Transition maps of the Henkin language chain

Equations

• One or more equations did not get rendered due to their size.
• NFChoice.Fol.henkinLanguageChainMaps L x✝ 0 H = ⋯ ▸ NFChoice.Fol.Lhom.id (NFChoice.Fol.henkinLanguageChainObjects x✝)

theorem NFChoice.Fol.henkin_language_chain_maps_inj (L : Language) (i j : ℕ) (h : i ≤ j) : (henkinLanguageChainMaps L i j h).IsInjective

theorem NFChoice.Fol.henkin_language_chain_maps_functorial (L : Language) (x y z : ℕ) (f1 : x ≤ y) (f2 : y ≤ z) (f3 : x ≤ z) : henkinLanguageChainMaps L x z f3 = (henkinLanguageChainMaps L y z f2).comp (henkinLanguageChainMaps L x y f1)

Functoriality of the Henkin language chain maps

@[reducible]

def NFChoice.Fol.henkinLanguageChain {L : Language} : DirectedDiagramLanguage

The Henkin language chain as a directed diagram of languages

Equations

• NFChoice.Fol.henkinLanguageChain = { obj := NFChoice.Fol.henkinLanguageChainObjects, mor := fun {x y : ℕ} (H : x ≤ y) => NFChoice.Fol.henkinLanguageChainMaps L x y H, h_mor := ⋯ }

theorem NFChoice.Fol.id_of_self_map (L : Language) (k : ℕ) : henkinLanguageChainMaps L k k ⋯ = Lhom.id (henkinLanguageChainObjects k)

theorem NFChoice.Fol.henkin_language_inclusion_chain_map {i : ℕ} {L : Language} : henkinLanguageInclusion = henkinLanguageChainMaps L i (i + 1) ⋯

The limit language L_∞

@[reducible]

def NFChoice.Fol.LInfty (L : Language) : Language

The colimit of the Henkin language chain

Equations

• NFChoice.Fol.LInfty L = NFChoice.Fol.colimitLanguage NFChoice.Fol.henkinLanguageChain

@[reducible]

def NFChoice.Fol.henkinLanguageCanonicalMap {L : Language} (m : ℕ) : henkinLanguageChain.obj m →ᴸ LInfty L

Canonical inclusion L_m → L_∞

Equations

• NFChoice.Fol.henkinLanguageCanonicalMap m = NFChoice.Fol.canonicalMapLanguage m

@[simp]

theorem NFChoice.Fol.henkin_language_canonical_map_inj {L : Language} (m : ℕ) : (henkinLanguageCanonicalMap m).IsInjective

Directed diagrams of terms and formulas

@[reducible]

def NFChoice.Fol.henkinTermChain {L : Language} (l : ℕ) : colimit.DirectedDiagram ℕ'

Chain of preterms at level l

Equations

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

@[reducible]

def NFChoice.Fol.henkinFormulaChain {L : Language} (l : ℕ) : colimit.DirectedDiagram ℕ'

Chain of preformulas at level l

Equations

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

@[reducible]

def NFChoice.Fol.henkinBoundedTermChain {L : Language} (n l : ℕ) : colimit.DirectedDiagram ℕ'

Chain of bounded preterms at bound n, level l

Equations

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

@[reducible]

def NFChoice.Fol.henkinBoundedTermChain' {L : Language} : colimit.DirectedDiagram ℕ'

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

Equations

• NFChoice.Fol.henkinBoundedTermChain' = NFChoice.Fol.henkinBoundedTermChain 1 0

@[reducible]

def NFChoice.Fol.henkinBoundedFormulaChain {L : Language} (n l : ℕ) : colimit.DirectedDiagram ℕ'

Chain of bounded preformulas at bound n, level l

Equations

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

@[reducible]

def NFChoice.Fol.henkinBoundedFormulaChain' {L : Language} : colimit.DirectedDiagram ℕ'

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

Equations

• NFChoice.Fol.henkinBoundedFormulaChain' = NFChoice.Fol.henkinBoundedFormulaChain 1 0

Cocones with vertex L_∞

def NFChoice.Fol.coconeOfLInfty {L : Language} : CoconeLanguage henkinLanguageChain

L_∞ is a cocone over the diagram of languages

Equations

• NFChoice.Fol.coconeOfLInfty = NFChoice.Fol.coconeOfColimitLanguage NFChoice.Fol.henkinLanguageChain

def NFChoice.Fol.coconeOfTermLInfty {L : Language} (l : ℕ) : colimit.cocone (henkinTermChain l)

Cocone over the preterm chain with vertex preterm (L_∞ L) l

Equations

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

def NFChoice.Fol.coconeOfFormulaLInfty {L : Language} (l : ℕ) : colimit.cocone (henkinFormulaChain l)

Cocone over the preformula chain with vertex @preformula (L_∞ L) l

Equations

• NFChoice.Fol.coconeOfFormulaLInfty l = { vertex := NFChoice.Fol.preformula l, map := fun (i : ℕ'.carrier) => (NFChoice.Fol.henkinLanguageCanonicalMap i).onFormula, h_compat := ⋯ }

def NFChoice.Fol.coconeOfBoundedTermLInfty {L : Language} (n l : ℕ) : colimit.cocone (henkinBoundedTermChain n l)

Cocone over the bounded term chain with vertex bounded_preterm (L_∞ L) n l

Equations

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

Cocone over the bounded formula chain (Task 16b,

src/henkin.lean:452-499)

def NFChoice.Fol.coconeOfBoundedFormulaLInfty {L : Language} (n l : ℕ) : colimit.cocone (henkinBoundedFormulaChain n l)

Cocone over the bounded preformula chain with vertex bounded_preformula (L_∞ L) n l

Equations

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

def NFChoice.Fol.coconeOfBoundedFormula'LInfty {L : Language} : colimit.cocone henkinBoundedFormulaChain'

bounded_formula (L_∞ L) 1 is naturally a cocone over the diagram of bounded_formulas

Equations

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

Comparison maps (universal maps from colimits to L_∞)

def NFChoice.Fol.term_comparison {L : Language} (l : ℕ) : colimit.LimitCarrier (henkinTermChain l) → preterm (LInfty L) l

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

Equations

• NFChoice.Fol.term_comparison l = NFChoice.colimit.universalMap

def NFChoice.Fol.formulaComparison {L : Language} (l : ℕ) : colimit.LimitCarrier (henkinFormulaChain l) → preformula l

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

Equations

• NFChoice.Fol.formulaComparison l = NFChoice.colimit.universalMap

def NFChoice.Fol.boundedTermComparison {L : Language} (n l : ℕ) : colimit.LimitCarrier (henkinBoundedTermChain n l) → BoundedPreterm (LInfty L) n l

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

Equations

• NFChoice.Fol.boundedTermComparison n l = NFChoice.colimit.universalMap

@[reducible]

def NFChoice.Fol.boundedTerm'Comparison {L : Language} : colimit.LimitCarrier henkinBoundedTermChain' → boundedTerm (LInfty L) 1

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

Equations

• NFChoice.Fol.boundedTerm'Comparison = NFChoice.Fol.boundedTermComparison 1 0

def NFChoice.Fol.boundedFormulaComparison {L : Language} (n l : ℕ) : colimit.LimitCarrier (henkinBoundedFormulaChain n l) → BoundedPreformula (LInfty L) n l

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

Equations

• NFChoice.Fol.boundedFormulaComparison n l = NFChoice.colimit.universalMap

@[reducible]

def NFChoice.Fol.boundedFormula'Comparison {L : Language} : colimit.LimitCarrier henkinBoundedFormulaChain' → boundedFormula (LInfty L) 1

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

Equations

• NFChoice.Fol.boundedFormula'Comparison = NFChoice.Fol.boundedFormulaComparison 1 0

Bijectivity of comparison maps (src/henkin.lean:508-655)

theorem NFChoice.Fol.term_comparison_bijective {L : Language} (l : ℕ) : Function.Bijective (term_comparison l)

theorem NFChoice.Fol.formula_comparison_bijective {L : Language} (l : ℕ) : Function.Bijective (formulaComparison l)

@[simp]

theorem NFChoice.Fol.bounded_term_comparison_bijective {L : Language} (n l : ℕ) : Function.Bijective (boundedTermComparison n l)

@[simp]

theorem NFChoice.Fol.bounded_formula_comparison_bijective {L : Language} (n l : ℕ) : Function.Bijective (boundedFormulaComparison n l)

theorem NFChoice.Fol.bounded_formula'_comparison_bijective {L : Language} : Function.Bijective boundedFormula'Comparison

noncomputable def NFChoice.Fol.equivBoundedFormulaComparison {L : Language} : colimit.LimitCarrier henkinBoundedFormulaChain' ≃ boundedFormula (LInfty L) 1

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

Equations

• NFChoice.Fol.equivBoundedFormulaComparison = Equiv.ofBijective NFChoice.Fol.boundedFormula'Comparison ⋯

Henkin theory chain (src/henkin.lean:661-734)

def NFChoice.Fol.henkinTheoryChain {L : Language} (T : SentTheory L) (n : ℕ) : SentTheory (henkinLanguageChain.obj n)

The Henkin theory chain: T_n = Henkin^n step applied to T

Equations

• NFChoice.Fol.henkinTheoryChain T 0 = T
• NFChoice.Fol.henkinTheoryChain T n.succ = NFChoice.Fol.henkinTheoryStep (NFChoice.Fol.henkinTheoryChain T n)

theorem NFChoice.Fol.is_consistent_henkin_theory_chain {L : Language} {T : SentTheory L} (hT : T.isConsistent) (n : ℕ) : (henkinTheoryChain T n).isConsistent

has_enough_constants (from src/fol.lean:2482)

def NFChoice.Fol.hasEnoughConstants {L : Language} (T : SentTheory L) : Prop

A theory has enough constants if every bounded formula has a Henkin witness

Equations

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

theorem NFChoice.Fol.hasEnoughConstants.intro {L : Language} (T : SentTheory L) (H : ∀ (f : boundedFormula L 1), ∃ (c : L.constants), provable T.fst (BoundedPreformula.fst (witProperty f c))) : hasEnoughConstants T

ι: pushing T_n into Theory L_∞

def NFChoice.Fol.ι {L : Language} {T : SentTheory L} (m : ℕ) : SentTheory (LInfty L)

Given T_n from henkin_theory_chain, ι T_n is the expansion of T_n to an L_infty theory

Equations

• NFChoice.Fol.ι m = (NFChoice.Fol.henkinLanguageCanonicalMap m).onSentence '' NFChoice.Fol.henkinTheoryChain T m

@[simp]

theorem NFChoice.Fol.in_iota_of_in_step {L : Language} (i : ℕ) {T : SentTheory L} (f : sentence (henkinLanguageChain.obj (i + 1))) : f ∈ henkinTheoryChain T (i + 1) → (henkinLanguageCanonicalMap (i + 1)).onBoundedFormula f ∈ ι (i + 1)

@[simp]

theorem NFChoice.Fol.is_consistent_iota {L : Language} {T : SentTheory L} (hT : T.isConsistent) (m : ℕ) : (ι m).isConsistent

Monotonicity: ι is increasing (src/henkin.lean:736-751)

theorem NFChoice.Fol.henkin_theory_chain_inclusion_step {L : Language} {T : SentTheory L} {i : ℕ} {f : sentence (henkinLanguageChain.obj i)} (hf : f ∈ henkinTheoryChain T i) : (henkinLanguageChainMaps L i (i + 1) ⋯).onBoundedFormula f ∈ henkinTheoryChain T (i + 1)

theorem NFChoice.Fol.iota_inclusion_of_le {L : Language} {T : SentTheory L} {i j : ℕ} : i ≤ j → ι i ⊆ ι j

T_infty: the henkinization (src/henkin.lean:753-774)

@[reducible]

def NFChoice.Fol.TInfty {L : Language} (T : SentTheory L) : SentTheory (LInfty L)

T_infty is the henkinization of T; we define it to be the union ⋃ (n : ℕ), ι(T n).

Equations

• NFChoice.Fol.TInfty T = ⋃ (n : ℕ), NFChoice.Fol.ι n

@[reducible]

def NFChoice.Fol.henkinLanguage {L : Language} {T : SentTheory L} {_hT : T.isConsistent} : Language

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

Equations

• NFChoice.Fol.henkinLanguage = NFChoice.Fol.LInfty L

def NFChoice.Fol.henkinLanguageOver {L : Language} {T : SentTheory L} {_hT : T.isConsistent} : L →ᴸ henkinLanguage

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

Equations

• NFChoice.Fol.henkinLanguageOver = NFChoice.Fol.henkinLanguageCanonicalMap 0

theorem NFChoice.Fol.henkin_language_over_injective {L : Language} {T : SentTheory L} {_hT : T.isConsistent} : henkinLanguageOver.IsInjective

@[reducible]

def NFChoice.Fol.henkinization {L : Language} {T : SentTheory L} (hT : T.isConsistent) : SentTheory henkinLanguage

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

Equations

• NFChoice.Fol.henkinization hT = NFChoice.Fol.TInfty T

wit_infty: find a Henkin witness in henkinization

(src/henkin.lean:778-783)

noncomputable def NFChoice.Fol.witInfty {L : Language} {T : SentTheory L} {hT : T.isConsistent} (f : boundedFormula henkinLanguage 1) : (c : henkinLanguage.constants) × (f' : (x : colimit.LimitCarrier henkinBoundedFormulaChain') ×' boundedFormula'Comparison x = f) × (f'' : colimit.coproductOfDirectedDiagram henkinBoundedFormulaChain') ×' ⟦f''⟧ = f'.fst ∧ c = (henkinLanguageCanonicalMap (f''.fst + 1)).onFunction (wit' f''.snd)

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

Equations

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

henkinization has enough constants

(src/henkin.lean:785-831)

@[simp]

theorem NFChoice.Fol.henkinization_is_henkin {L : Language} {T : SentTheory L} (hT : T.isConsistent) : hasEnoughConstants (henkinization hT)

Directed union infrastructure (src/henkin.lean:833-874)

def NFChoice.Fol.henkinTheoryOver {L : Language} (T : SentTheory L) (hT : T.isConsistent) (n : ℕ) : TheoryOver (ι 0) ⋯

For every n, T_n as a Theory_over (ι T 0)

Equations

• NFChoice.Fol.henkinTheoryOver T hT n = ⟨NFChoice.Fol.ι n, ⋯⟩

def NFChoice.Fol.henkinTheorySchain {L : Language} (T : SentTheory L) (hT : T.isConsistent) : Set (TheoryOver (ι 0) ⋯)

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

Equations

• NFChoice.Fol.henkinTheorySchain T hT = {T' : NFChoice.Fol.TheoryOver (NFChoice.Fol.ι 0) ⋯ | ∃ (k : ℕ), NFChoice.Fol.ι k = ↑T'}

theorem NFChoice.Fol.iota_union_rw {L : Language} (T : SentTheory L) (hT : T.isConsistent) : ι 0 ∪ ⋃₀ (Subtype.val '' henkinTheorySchain T hT) = henkinization hT

theorem NFChoice.Fol.chain_henkin_theory_chain {L : Language} (T : SentTheory L) (hT : T.isConsistent) : IsChain TheoryOverSubset (henkinTheorySchain T hT)

theorem NFChoice.Fol.is_consistent_henkinization {L : Language} {T : SentTheory L} (hT : T.isConsistent) : (henkinization hT).isConsistent

Completion of henkinization (src/henkin.lean:891-911)

noncomputable def NFChoice.Fol.completionOfHenkinizationCore {L : Language} {T : SentTheory L} (hT : T.isConsistent) : (T' : TheoryOver (henkinization hT) ⋯) ×' (↑T').isComplete

The core completion: henkinization extends to a complete consistent theory

Equations

• NFChoice.Fol.completionOfHenkinizationCore hT = NFChoice.Fol.completionOfConsis (NFChoice.Fol.henkinization hT) ⋯

noncomputable def NFChoice.Fol.completionOfHenkinization {L : Language} {T : SentTheory L} (hT : T.isConsistent) : SentTheory henkinLanguage

The completed henkinization theory

Equations

• NFChoice.Fol.completionOfHenkinization hT = ↑(NFChoice.Fol.completionOfHenkinizationCore hT).fst

theorem NFChoice.Fol.completion_of_henkinization_contains {L : Language} {T : SentTheory L} (hT : T.isConsistent) : henkinization hT ⊆ completionOfHenkinization hT

The completed theory contains the henkinization

theorem NFChoice.Fol.completion_of_henkinization_consistent {L : Language} {T : SentTheory L} (hT : T.isConsistent) : (completionOfHenkinization hT).isConsistent

The completed theory is consistent

theorem NFChoice.Fol.completion_of_henkinization_complete {L : Language} {T : SentTheory L} (hT : T.isConsistent) : (completionOfHenkinization hT).isComplete

The completed theory is complete

@[simp]

theorem NFChoice.Fol.completion_of_henkinization_is_henkin {L : Language} {T : SentTheory L} (hT : T.isConsistent) : hasEnoughConstants (completionOfHenkinization hT)

The completed theory is Henkin

Helpers for the term model (ported from

src/fol.lean:2445-2498)

theorem NFChoice.Fol.mem_of_sprovable {L : Language} {T : SentTheory L} (hcomp : T.isComplete) {f : sentence L} (hf : T.sprovable f) : f ∈ T

If T is complete and T ⊢ₛ' f, then f ∈ T

theorem NFChoice.Fol.notI_of_is_complete {L : Language} {T : SentTheory L} (hcomp : T.isComplete) {f : sentence L} (hf : ¬T.sprovable f) : T.sprovable (bdNot f)

If T is complete and T ⊬ₛ' f, then T ⊢ₛ' bd_not f

theorem NFChoice.Fol.impI_of_is_complete {L : Language} {T : SentTheory L} (hcomp : T.isComplete) {φ ψ : sentence L} (h : T.sprovable φ → T.sprovable ψ) : T.sprovable (bd_imp φ ψ)

If T is complete, T ⊢ₛ' (bd_imp φ ψ) follows from (T ⊢ₛ' φ → T ⊢ₛ' ψ)

theorem NFChoice.Fol.find_counterexample_of_henkin {L : Language} {T : SentTheory L} (hcomp : T.isComplete) (henk : hasEnoughConstants T) (f : boundedFormula L 1) (hf : ¬T.sprovable (bd_all f)) : ∃ (t : closedTerm L), T.sprovable (bdNot (subst0BoundedFormula f t))

Given a complete Henkin theory, universal failure yields a counterexample

Term model construction (src/fol.lean:2500-2559)

def NFChoice.Fol.term_rel {L : Language} (T : SentTheory L) (t₁ t₂ : closedTerm L) : Prop

The term equality relation: t₁ ~ t₂ iff T ⊢ₛ' t₁ ≃ t₂

Equations

• NFChoice.Fol.term_rel T t₁ t₂ = T.sprovable (NFChoice.Fol.bd_equal t₁ t₂)

noncomputable def NFChoice.Fol.term_setoid {L : Language} (T : SentTheory L) : Setoid (closedTerm L)

The term equality setoid

Equations

• NFChoice.Fol.term_setoid T = { r := NFChoice.Fol.term_rel T, iseqv := ⋯ }

@[reducible, inline]

noncomputable abbrev NFChoice.Fol.termModel' {L : Language} (T : SentTheory L) : Type u

The carrier of the term model: closed terms modulo provable equality

Equations

• NFChoice.Fol.termModel' T = Quotient (NFChoice.Fol.term_setoid T)

noncomputable def NFChoice.Fol.term_model_fun' {L : Language} (T : SentTheory L) {l : ℕ} (t : closedPreterm L l) (ts : DVec (closedTerm L) l) : termModel' T

The function interpretation helper for the term model

Equations

• NFChoice.Fol.term_model_fun' T t ts = Quotient.mk'' (NFChoice.Fol.bdApps t ts)

theorem NFChoice.Fol.term_model_fun'_congr {L : Language} {T : SentTheory L} {l : ℕ} (t : closedPreterm L l) {xs xs' : DVec (closedTerm L) l} : xs.DVecRel xs' → term_model_fun' T t xs = term_model_fun' T t xs'

Helper: term_model_fun' is compatible with term_rel on each argument

noncomputable def NFChoice.Fol.term_model_fun {L : Language} (T : SentTheory L) {l : ℕ} (t : closedPreterm L l) (ts : DVec (termModel' T) l) : termModel' T

The function interpretation in the term model, using quotient_lift

Equations

• NFChoice.Fol.term_model_fun T t ts = NFChoice.DVec.quotientLift (NFChoice.Fol.term_model_fun' T t) ⋯ ts

noncomputable def NFChoice.Fol.term_model_rel' {L : Language} (T : SentTheory L) {l : ℕ} (f : presentence L l) (ts : DVec (closedTerm L) l) : Prop

The relation interpretation helper

Equations

• NFChoice.Fol.term_model_rel' T f ts = T.sprovable (NFChoice.Fol.bdAppsRel f ts)

theorem NFChoice.Fol.term_model_rel'_congr {L : Language} {T : SentTheory L} {l : ℕ} (f : presentence L l) {xs xs' : DVec (closedTerm L) l} : xs.DVecRel xs' → term_model_rel' T f xs = term_model_rel' T f xs'

Helper: term_model_rel' is compatible with term_rel on each argument

noncomputable def NFChoice.Fol.term_model_rel {L : Language} (T : SentTheory L) {l : ℕ} (f : presentence L l) (ts : DVec (termModel' T) l) : Prop

The relation interpretation in the term model

Equations

• NFChoice.Fol.term_model_rel T f ts = NFChoice.DVec.quotientLift (NFChoice.Fol.term_model_rel' T f) ⋯ ts

Term model and main completeness theorem

@[reducible]

noncomputable def NFChoice.Fol.term_model {L : Language} {T : SentTheory L} (_hcomp : T.isComplete) (_henk : hasEnoughConstants T) : Structure L

term_model of a complete Henkin theory (src/fol.lean:2559-2562)

Equations

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

@[reducible]

noncomputable def NFChoice.Fol.term_mk {L : Language} (T : SentTheory L) (t : closedTerm L) : termModel' T

Canonical quotient map from closed terms to the term model

Equations

• NFChoice.Fol.term_mk T t = Quotient.mk'' t

Realization in the term model (src/fol.lean:2568-2627)

theorem NFChoice.Fol.term_model_ssatisfied_iff_struct {L : Language} {T : SentTheory L} (hcomp : T.isComplete) (henk : hasEnoughConstants T) (n : ℕ) (n_ih : ∀ m < n, ∀ {l' : ℕ} (f' : presentence L l') (ts' : DVec (closedTerm L) l'), countQuantifiers (BoundedPreformula.fst f') < m → (T.sprovable (bdAppsRel f' ts') ↔ realizeSentence (term_model hcomp henk) (bdAppsRel f' ts'))) {l : ℕ} (f : BoundedPreformula L 0 l) (ts : DVec (closedTerm L) l) : countQuantifiers f.fst < n → (T.sprovable (bdAppsRel f ts) ↔ realizeSentence (term_model hcomp henk) (bdAppsRel f ts))

Structural recursion on a bounded_preformula L 0 l for the term-model iff, parameterized by an external IH on smaller quantifier-counts.

Implemented via direct structural pattern matching on `f` to
avoid issues
with `induction` on a non-variable index `n = 0`. 

theorem NFChoice.Fol.term_model_ssatisfied {L : Language} {T : SentTheory L} (hcomp : T.isComplete) (henk : hasEnoughConstants T) : allRealizeSentence (term_model hcomp henk) T

The term model satisfies T (src/fol.lean:2672)

@[simp]

theorem NFChoice.Fol.reduct_of_complete_henkinization_models_T {L : Language} {T : SentTheory L} (hT : T.isConsistent) : allRealizeSentence (term_model ⋯ ⋯[[henkinLanguageCanonicalMap 0]]) T

The reduct of the term model of the complete henkinization satisfies T

@[simp]

theorem NFChoice.Fol.reduct_of_complete_henkinization_satisfies {L : Language} {T : SentTheory L} (hT : T.isConsistent) (ψ : sentence L) (hψ : ψ ∈ T) : realizeSentence (term_model ⋯ ⋯[[henkinLanguageCanonicalMap 0]]) ψ

Given ψ ∈ T, the term model satisfies ψ