Flypitch.Henkin constructs the omega-chain of language extensions that adjoin witness constants, forms its colimit language LInfty, and compares the colimit syntax with the bounded syntax already present in the tower. The later part of the file packages these maps into the Henkin theory used by the completeness argument.

structure Flypitch.colimit.directed_diagram_language (D : directed_type) : Type ((max u v) + 1)

• obj : D.carrier → fol.Language
• mor {x y : D.carrier} : D.rel x y → (self.obj x →ᴸ self.obj y)
• h_mor {x y z : D.carrier} {f₁ : D.rel x y} {f₂ : D.rel y z} {f₃ : D.rel x z} : self.mor f₃ = (self.mor f₂).comp (self.mor f₁)

@[reducible]

def Flypitch.colimit.diagram_functions {D : directed_type} {F : directed_diagram_language D} (n : ℕ) : directed_diagram D

Equations

• Flypitch.colimit.diagram_functions n = { obj := fun (x : D.carrier) => (F.obj x).functions n, mor := fun {x y : D.carrier} (h : D.rel x y) => (F.mor h).on_function, h_mor := ⋯ }

@[reducible]

def Flypitch.colimit.diagram_relations {D : directed_type} {F : directed_diagram_language D} (n : ℕ) : directed_diagram D

Equations

• Flypitch.colimit.diagram_relations n = { obj := fun (x : D.carrier) => (F.obj x).relations n, mor := fun {x y : D.carrier} (h : D.rel x y) => (F.mor h).on_relation, h_mor := ⋯ }

def Flypitch.colimit.colimit_language {D : directed_type} (F : directed_diagram_language D) : fol.Language

Equations

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

def Flypitch.colimit.canonical_map_language {D : directed_type} {F : directed_diagram_language D} (i : D.carrier) : F.obj i →ᴸ colimit_language F

Equations

• Flypitch.colimit.canonical_map_language i = { on_function := fun {n : ℕ} => Flypitch.colimit.canonical_map i, on_relation := fun {n : ℕ} => Flypitch.colimit.canonical_map i }

structure Flypitch.colimit.cocone_language {D : directed_type} (F : directed_diagram_language D) : Type (max u (u_1 + 1))

• vertex : fol.Language
• map (i : D.carrier) : F.obj i →ᴸ self.vertex
• h_compat {i j : D.carrier} (h : D.rel i j) : self.map i = (self.map j).comp (F.mor h)

def Flypitch.colimit.cocone_of_colimit_language {D : directed_type} (F : directed_diagram_language D) : cocone_language F

Equations

• Flypitch.colimit.cocone_of_colimit_language F = { vertex := Flypitch.colimit.colimit_language F, map := Flypitch.colimit.canonical_map_language, h_compat := ⋯ }

def Flypitch.colimit.universal_map_language {D : directed_type} {F : directed_diagram_language D} {V : cocone_language F} : colimit_language F →ᴸ V.vertex

Equations

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

inductive Flypitch.henkin.languageFunctions (L : fol.Language) : ℕ → Type u

• inc {L : fol.Language} {n : ℕ} : L.functions n → languageFunctions L n
• wit {L : fol.Language} : fol.bounded_formula L 1 → languageFunctions L 0

@[reducible]

def Flypitch.henkin.languageStep (L : fol.Language) : fol.Language

Equations

• Flypitch.henkin.languageStep L = { functions := Flypitch.henkin.languageFunctions L, relations := L.relations }

def Flypitch.henkin.wit' {L : fol.Language} : fol.bounded_formula L 1 → (languageStep L).constants

Equations

• Flypitch.henkin.wit' = Flypitch.henkin.languageFunctions.wit

def Flypitch.henkin.inclusion {L : fol.Language} : L →ᴸ languageStep L

Equations

• Flypitch.henkin.inclusion = { on_function := fun {_n : ℕ} (f : L.functions _n) => Flypitch.henkin.languageFunctions.inc f, on_relation := fun {_n : ℕ} (R : L.relations _n) => R }

theorem Flypitch.henkin.inclusion_inj {L : fol.Language} : inclusion.is_injective

@[reducible]

def Flypitch.henkin.chainObjects (L : fol.Language) : ℕ → fol.Language

Equations

• Flypitch.henkin.chainObjects L 0 = L
• Flypitch.henkin.chainObjects L n.succ = Flypitch.henkin.languageStep (Flypitch.henkin.chainObjects L n)

def Flypitch.henkin.chainMaps (L : fol.Language) (x y : ℕ) : x ≤ y → (chainObjects L x →ᴸ chainObjects L y)

Equations

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

theorem Flypitch.henkin.chainMaps_comp (L : fol.Language) {x y z : ℕ} (f₁ : x ≤ y) (f₂ : y ≤ z) : chainMaps L x z ⋯ = (chainMaps L y z f₂).comp (chainMaps L x y f₁)

theorem Flypitch.henkin.chainMaps_inj (L : fol.Language) (x y : ℕ) (h : x ≤ y) : (chainMaps L x y h).is_injective

def Flypitch.henkin.languageChain {L : fol.Language} : colimit.directed_diagram_language ℕ'

Equations

• Flypitch.henkin.languageChain = { obj := Flypitch.henkin.chainObjects L, mor := fun {x y : ℕ'.carrier} (h : ℕ'.rel x y) => Flypitch.henkin.chainMaps L x y h, h_mor := ⋯ }

def Flypitch.henkin.LInfty (L : fol.Language) : fol.Language

Equations

• Flypitch.henkin.LInfty L = Flypitch.colimit.colimit_language Flypitch.henkin.languageChain

def Flypitch.henkin.canonicalMap {L : fol.Language} (m : ℕ) : chainObjects L m →ᴸ LInfty L

Equations

• Flypitch.henkin.canonicalMap m = Flypitch.colimit.canonical_map_language m

theorem Flypitch.henkin.canonicalMap_inj {L : fol.Language} (m : ℕ) : (canonicalMap m).is_injective

def Flypitch.henkin.termChain {L : fol.Language} (l : ℕ) : colimit.directed_diagram ℕ'

Equations

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

def Flypitch.henkin.formulaChain {L : fol.Language} (l : ℕ) : colimit.directed_diagram ℕ'

Equations

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

def Flypitch.henkin.boundedTermChain {L : fol.Language} (n l : ℕ) : colimit.directed_diagram ℕ'

Equations

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

@[reducible]

def Flypitch.henkin.boundedTermChain' {L : fol.Language} : colimit.directed_diagram ℕ'

Equations

• Flypitch.henkin.boundedTermChain' = Flypitch.henkin.boundedTermChain 1 0

def Flypitch.henkin.boundedFormulaChain {L : fol.Language} (n l : ℕ) : colimit.directed_diagram ℕ'

Equations

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

@[reducible]

def Flypitch.henkin.boundedFormulaChain' {L : fol.Language} : colimit.directed_diagram ℕ'

Equations

• Flypitch.henkin.boundedFormulaChain' = Flypitch.henkin.boundedFormulaChain 1 0

def Flypitch.henkin.coconeOfLInfty {L : fol.Language} : colimit.cocone_language languageChain

Equations

• Flypitch.henkin.coconeOfLInfty = Flypitch.colimit.cocone_of_colimit_language Flypitch.henkin.languageChain

def Flypitch.henkin.coconeOfTermLInfty {L : fol.Language} (l : ℕ) : colimit.cocone (termChain l)

Equations

• Flypitch.henkin.coconeOfTermLInfty l = { vertex := Flypitch.fol.preterm (Flypitch.henkin.LInfty L) l, map := fun (i : ℕ'.carrier) => (Flypitch.henkin.canonicalMap i).on_term, h_compat := ⋯ }

def Flypitch.henkin.coconeOfFormulaLInfty {L : fol.Language} (l : ℕ) : colimit.cocone (formulaChain l)

Equations

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

def Flypitch.henkin.coconeOfBoundedTermLInfty {L : fol.Language} (n l : ℕ) : colimit.cocone (boundedTermChain n l)

Equations

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

def Flypitch.henkin.coconeOfBoundedFormulaLInfty {L : fol.Language} (n l : ℕ) : colimit.cocone (boundedFormulaChain n l)

Equations

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

def Flypitch.henkin.coconeOfBoundedFormulaPrimeLInfty {L : fol.Language} : colimit.cocone boundedFormulaChain'

Equations

• Flypitch.henkin.coconeOfBoundedFormulaPrimeLInfty = id (Flypitch.henkin.coconeOfBoundedFormulaLInfty 1 0)

def Flypitch.henkin.termComparison {L : fol.Language} (l : ℕ) : colimit.colimit (termChain l) → fol.preterm (LInfty L) l

Equations

• Flypitch.henkin.termComparison l = Flypitch.colimit.universal_map

def Flypitch.henkin.formulaComparison {L : fol.Language} (l : ℕ) : colimit.colimit (formulaChain l) → fol.preformula (LInfty L) l

Equations

• Flypitch.henkin.formulaComparison l = Flypitch.colimit.universal_map

def Flypitch.henkin.boundedTermComparison {L : fol.Language} (n l : ℕ) : colimit.colimit (boundedTermChain n l) → fol.bounded_preterm (LInfty L) n l

Equations

• Flypitch.henkin.boundedTermComparison n l = Flypitch.colimit.universal_map

@[reducible]

def Flypitch.henkin.boundedTermComparison' {L : fol.Language} : colimit.colimit boundedTermChain' → fol.bounded_term (LInfty L) 1

Equations

• Flypitch.henkin.boundedTermComparison' = Flypitch.henkin.boundedTermComparison 1 0

def Flypitch.henkin.boundedFormulaComparison {L : fol.Language} (n l : ℕ) : colimit.colimit (boundedFormulaChain n l) → fol.bounded_preformula (LInfty L) n l

Equations

• Flypitch.henkin.boundedFormulaComparison n l = Flypitch.colimit.universal_map

@[reducible]

def Flypitch.henkin.boundedFormulaComparison' {L : fol.Language} : colimit.colimit boundedFormulaChain' → fol.bounded_formula (LInfty L) 1

Equations

• Flypitch.henkin.boundedFormulaComparison' = Flypitch.henkin.boundedFormulaComparison 1 0

theorem Flypitch.henkin.termComparison_bijective {L : fol.Language} (l : ℕ) : Function.Bijective (termComparison l)

theorem Flypitch.henkin.formulaComparison_bijective {L : fol.Language} (l : ℕ) : Function.Bijective (formulaComparison l)

theorem Flypitch.henkin.boundedTermComparison_bijective {L : fol.Language} (n l : ℕ) : Function.Bijective (boundedTermComparison n l)

theorem Flypitch.henkin.boundedFormulaComparison_bijective {L : fol.Language} (n l : ℕ) : Function.Bijective (boundedFormulaComparison n l)

theorem Flypitch.henkin.boundedFormulaComparison'_bijective {L : fol.Language} : Function.Bijective boundedFormulaComparison'

noncomputable def Flypitch.henkin.equivBoundedFormulaComparison {L : fol.Language} : colimit.colimit boundedFormulaChain' ≃ fol.bounded_formula (LInfty L) 1

Equations

• Flypitch.henkin.equivBoundedFormulaComparison = Equiv.ofBijective Flypitch.henkin.boundedFormulaComparison' ⋯

@[reducible]

def Flypitch.henkin.witProperty {L : fol.Language} (f : fol.bounded_formula L 1) (c : L.constants) : fol.sentence L

Equations

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

def Flypitch.henkin.has_enough_constants {L : fol.Language} (T : fol.Theory L) : Prop

Equations

• Flypitch.henkin.has_enough_constants T = ∃ (C : Flypitch.fol.bounded_formula L 1 → L.constants), ∀ (f : Flypitch.fol.bounded_formula L 1), T ⊢' Flypitch.henkin.witProperty f (C f)

theorem Flypitch.henkin.has_enough_constants.intro {L : fol.Language} (T : fol.Theory L) (H : ∀ (f : fol.bounded_formula L 1), ∃ (c : L.constants), T ⊢' witProperty f c) : has_enough_constants T

theorem Flypitch.henkin.has_enough_constants_of_subset {L : fol.Language} {T T' : fol.Theory L} (hsub : T.Subset T') (hT : has_enough_constants T) : has_enough_constants T'

def Flypitch.henkin.henkinTheoryStep {L : fol.Language} (T : fol.Theory L) : fol.Theory (languageStep L)

Equations

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

def Flypitch.henkin.henkinTheoryChain {L : fol.Language} (T : fol.Theory L) (n : ℕ) : fol.Theory (chainObjects L n)

Equations

• Flypitch.henkin.henkinTheoryChain T 0 = T
• Flypitch.henkin.henkinTheoryChain T n.succ = Flypitch.henkin.henkinTheoryStep (Flypitch.henkin.henkinTheoryChain T n)

@[reducible]

def Flypitch.henkin.henkinWitnessBody {L : fol.Language} (f : fol.bounded_formula L 1) : fol.bounded_formula L 1

The one-variable formula whose existential closure is always provable in the witness step.

Equations

• Flypitch.henkin.henkinWitnessBody f = Flypitch.fol.bd_imp (Flypitch.fol.bounded_preformula.cast1 (Flypitch.fol.bd_ex f)) f

@[reducible]

def Flypitch.henkin.henkinWitnessSentence {L : fol.Language} (f : fol.bounded_formula L 1) : fol.sentence (languageStep L)

The concrete witness axiom adjoined for f in henkinTheoryStep.

Equations

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

theorem Flypitch.henkin.henkinWitnessSentence_eq_witProperty {L : fol.Language} (f : fol.bounded_formula L 1) : henkinWitnessSentence f = witProperty (inclusion.on_bounded_formula f) (wit' f)

The explicit witness sentence agrees with the older witProperty presentation.

noncomputable def Flypitch.henkin.provable_henkinWitnessBody {L : fol.Language} {T : fol.Theory L} (f : fol.bounded_formula L 1) : T ⊢ fol.bd_ex (henkinWitnessBody f)

The standard existential premise used to show a Henkin witness step is admissible.

Equations

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

theorem Flypitch.henkin.wit_not_mem_range_inclusion {L : fol.Language} (f : fol.bounded_formula L 1) : wit' f ∉ Set.range inclusion.on_function

theorem Flypitch.henkin.wit_not_mem_symbols_witnessBody {L : fol.Language} (ψ ψ' : fol.bounded_formula L 1) : Sum.inl ⟨0, wit' ψ⟩ ∉ fol.symbols_in_formula (inclusion.on_bounded_formula ψ').fst

theorem Flypitch.henkin.wit_not_mem_symbols_witProperty_of_ne {L : fol.Language} {ψ ψ' : fol.bounded_formula L 1} (hneq : ψ' ≠ ψ) : Sum.inl ⟨0, wit' ψ⟩ ∉ fol.symbols_in_formula ↑(witProperty (inclusion.on_bounded_formula ψ') (wit' ψ'))

theorem Flypitch.henkin.wit_not_mem_symbols_henkinWitnessBody {L : fol.Language} (ψ : fol.bounded_formula L 1) : Sum.inl ⟨0, wit' ψ⟩ ∉ fol.symbols_in_formula (fol.bounded_preformula.fst (henkinWitnessBody (inclusion.on_bounded_formula ψ)))

theorem Flypitch.henkin.is_consistent_henkinTheoryStep {L : fol.Language} {T : fol.Theory L} (hT : fol.is_consistent T) : fol.is_consistent (henkinTheoryStep T)

def Flypitch.henkin.iota {L : fol.Language} {T : fol.Theory L} (m : ℕ) : fol.Theory (LInfty L)

Equations

• Flypitch.henkin.iota m = (Flypitch.henkin.canonicalMap m).Theory_induced (Flypitch.henkin.henkinTheoryChain T m)

def Flypitch.henkin.TInfty {L : fol.Language} (T : fol.Theory L) : fol.Theory (LInfty L)

Equations

• Flypitch.henkin.TInfty T = { carrier := ⋃ (n : ℕ), (Flypitch.henkin.iota n).carrier }

@[reducible]

def Flypitch.henkin.henkinLanguage {L : fol.Language} (T : fol.Theory L) : fol.Language

Equations

• Flypitch.henkin.henkinLanguage T = Flypitch.henkin.LInfty L

def Flypitch.henkin.henkinLanguageOver {L : fol.Language} {T : fol.Theory L} : L →ᴸ henkinLanguage T

Equations

• Flypitch.henkin.henkinLanguageOver = id (Flypitch.henkin.canonicalMap 0)

theorem Flypitch.henkin.henkinLanguageOver_injective {L : fol.Language} {T : fol.Theory L} : henkinLanguageOver.is_injective

def Flypitch.henkin.completeHenkinTheoryOver {L : fol.Language} (T : fol.Theory L) (hT : fol.is_consistent T) : Type (u + 1)

Equations

• Flypitch.henkin.completeHenkinTheoryOver T hT = ((T' : Flypitch.fol.Theory_over T hT) ×' Flypitch.henkin.has_enough_constants ↑T' ∧ Flypitch.fol.is_complete ↑T')

@[reducible]

def Flypitch.henkin.henkinization {L : fol.Language} {T : fol.Theory L} (hT : fol.is_consistent T) : fol.Theory (henkinLanguage T)

Equations

• Flypitch.henkin.henkinization hT = Flypitch.henkin.TInfty T

noncomputable def Flypitch.henkin.witInfty {L : fol.Language} (f : fol.bounded_formula (LInfty L) 1) : (c : (LInfty L).constants) × (f' : (x : colimit.colimit boundedFormulaChain') ×' equivBoundedFormulaComparison x = f) × (f'' : colimit.coproduct_of_directed_diagram boundedFormulaChain') ×' Quotient.mk'' f'' = f'.fst ∧ c = (canonicalMap (f''.fst + 1)).on_function (wit' f''.snd)

Equations

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

theorem Flypitch.henkin.inIotaOfInStep {L : fol.Language} {T : fol.Theory L} (i : ℕ) (f : fol.sentence (chainObjects L (i + 1))) (hf : f ∈ henkinTheoryChain T (i + 1)) : (canonicalMap (i + 1)).on_sentence f ∈ iota (i + 1)

@[simp]

theorem Flypitch.henkin.henkinizationIsHenkin {L : fol.Language} {T : fol.Theory L} (hT : fol.is_consistent T) : has_enough_constants (henkinization hT)

theorem Flypitch.henkin.henkinTheoryChainInclusionStep {L : fol.Language} {T : fol.Theory L} {i : ℕ} {f : fol.sentence (chainObjects L i)} (hf : f ∈ henkinTheoryChain T i) : inclusion.on_sentence f ∈ henkinTheoryChain T (i + 1)

theorem Flypitch.henkin.henkinTheoryChainInclusion {L : fol.Language} {T : fol.Theory L} {i j : ℕ} (h : i ≤ j) {f : fol.sentence (chainObjects L i)} : f ∈ henkinTheoryChain T i → (chainMaps L i j h).on_sentence f ∈ henkinTheoryChain T j

theorem Flypitch.henkin.iotaInclusionOfLe {L : fol.Language} {T : fol.Theory L} {i j : ℕ} : i ≤ j → (iota i).Subset (iota j)

theorem Flypitch.henkin.is_consistent_henkinTheoryChain {L : fol.Language} {T : fol.Theory L} (hT : fol.is_consistent T) (n : ℕ) : fol.is_consistent (henkinTheoryChain T n)

theorem Flypitch.henkin.is_consistent_iota {L : fol.Language} {T : fol.Theory L} (hT : fol.is_consistent T) (n : ℕ) : fol.is_consistent (iota n)

theorem Flypitch.henkin.finite_subset_iota_of_mem_TInfty {L : fol.Language} {T : fol.Theory L} (Γ : Finset (fol.sentence (LInfty L))) (hΓ : ↑Γ ⊆ (TInfty T).carrier) : ∃ (n : ℕ), ↑Γ ⊆ (iota n).carrier

theorem Flypitch.henkin.is_consistent_TInfty {L : fol.Language} {T : fol.Theory L} (hT : fol.is_consistent T) : fol.is_consistent (TInfty T)

theorem Flypitch.henkin.is_consistent_henkinization {L : fol.Language} {T : fol.Theory L} (hT : fol.is_consistent T) : fol.is_consistent (henkinization hT)

The Henkinization of a consistent theory is itself consistent.

noncomputable def Flypitch.henkin.completeHenkinizationOfConsis {L : fol.Language} {T : fol.Theory L} (hT : fol.is_consistent T) : completeHenkinTheoryOver (henkinization hT) ⋯

Complete a consistent Henkinization to a complete Henkin theory over it.

Equations

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