@[simp]

theorem Flypitch.fol.Theory.union_singleton_eq_insert {L : Language} (T : Theory L) (f : sentence L) : T ∪ {f} = insert f T

theorem Flypitch.fol.inconsis_not_of_provable {L : Language} {T : Theory L} {f : sentence L} : T ⊢' f → ¬is_consistent (T ∪ {∼f})

theorem Flypitch.fol.provable_of_inconsis_not {L : Language} {T : Theory L} {f : sentence L} : ¬is_consistent (T ∪ {∼f}) → T ⊢' f

theorem Flypitch.fol.can_extend {L : Language} (T : Theory L) (ψ : sentence L) (h : is_consistent T) : is_consistent (T ∪ {ψ}) ∨ is_consistent (T ∪ {∼ψ})

Given a theory T and a sentence ψ, either T ∪ {ψ} or T ∪ {∼ψ} is consistent.

@[reducible, inline]

abbrev Flypitch.fol.Theory_over {L : Language} (T : Theory L) (hT : is_consistent T) : Type (u + 1)

Equations

• Flypitch.fol.Theory_over T hT = Flypitch.fol.TheoryOver T hT

def Flypitch.fol.TheoryOverSubset {L : Language} {T : Theory L} {hT : is_consistent T} : TheoryOver T hT → TheoryOver T hT → Prop

Equations

• Flypitch.fol.TheoryOverSubset T₁ T₂ = (↑T₁).Subset ↑T₂

@[reducible, inline]

abbrev Flypitch.fol.Theory_over_subset {L : Language} {T : Theory L} {hT : is_consistent T} : TheoryOver T hT → TheoryOver T hT → Prop

Equations

• Flypitch.fol.Theory_over_subset = Flypitch.fol.TheoryOverSubset

@[implicit_reducible]

instance Flypitch.fol.instHasSubsetTheoryOver {L : Language} {T : Theory L} {hT : is_consistent T} : HasSubset (TheoryOver T hT)

Equations

• Flypitch.fol.instHasSubsetTheoryOver = { Subset := Flypitch.fol.TheoryOverSubset }

theorem Flypitch.fol.instReflTheoryOverTheoryOverSubset {L : Language} {T : Theory L} {hT : is_consistent T} : Std.Refl TheoryOverSubset

def Flypitch.fol.chainTheoryUnion {L : Language} {T : Theory L} {hT : is_consistent T} (c : Set (TheoryOver T hT)) : Theory L

Equations

• Flypitch.fol.chainTheoryUnion c = { carrier := ⋃₀ ((fun (U : Flypitch.fol.TheoryOver T hT) => (↑U).carrier) '' c) }

def Flypitch.fol.limitTheory {L : Language} {T : Theory L} {hT : is_consistent T} (c : Set (TheoryOver T hT)) : Theory L

Equations

• Flypitch.fol.limitTheory c = T ∪ Flypitch.fol.chainTheoryUnion c

theorem Flypitch.fol.mem_chainTheoryUnion_iff {L : Language} {T : Theory L} {hT : is_consistent T} {c : Set (TheoryOver T hT)} {ψ : sentence L} : ψ ∈ chainTheoryUnion c ↔ ∃ U ∈ c, ψ ∈ ↑U

theorem Flypitch.fol.finite_subset_limitTheory {L : Language} {T : Theory L} {hT : is_consistent T} {c : Set (TheoryOver T hT)} (hc : IsChain TheoryOverSubset c) (hcne : c.Nonempty) (Γ : Finset (sentence L)) (hΓ : ↑Γ ⊆ (limitTheory c).carrier) : ∃ U ∈ c, ↑Γ ⊆ (↑U).carrier

theorem Flypitch.fol.consis_limit {L : Language} {T : Theory L} {hT : is_consistent T} (c : Set (TheoryOver T hT)) (hc : IsChain TheoryOverSubset c) : is_consistent (limitTheory c)

noncomputable def Flypitch.fol.limit_theory {L : Language} {T : Theory L} {hT : is_consistent T} (c : Set (TheoryOver T hT)) (hc : IsChain TheoryOverSubset c) : (U : TheoryOver T hT) ×' ∀ U' ∈ c, TheoryOverSubset U' U

Equations

• Flypitch.fol.limit_theory c hc = ⟨⟨Flypitch.fol.limitTheory c, ⋯⟩, ⋯⟩

theorem Flypitch.fol.can_use_zorn {L : Language} {T : Theory L} {hT : is_consistent T} : (∀ (c : Set (TheoryOver T hT)), IsChain TheoryOverSubset c → ∃ (ub : TheoryOver T hT), ∀ a ∈ c, TheoryOverSubset a ub) ∧ ∀ (a b c : TheoryOver T hT), TheoryOverSubset a b → TheoryOverSubset b c → TheoryOverSubset a c

noncomputable def Flypitch.fol.maximal_extension {L : Language} (T : Theory L) (hT : is_consistent T) : (T_max : TheoryOver T hT) ×' ∀ (T' : TheoryOver T hT), TheoryOverSubset T_max T' → TheoryOverSubset T' T_max

Given a consistent theory, return a maximal consistent extension of it.

Equations

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

theorem Flypitch.fol.cannot_extend_maximal_extension {L : Language} {T : Theory L} {hT : is_consistent T} (T_max' : (T_max : TheoryOver T hT) ×' ∀ (T' : TheoryOver T hT), TheoryOverSubset T_max T' → TheoryOverSubset T' T_max) (ψ : sentence L) (hCons : is_consistent (↑T_max'.fst ∪ {ψ})) (hNot : ψ ∉ ↑T_max'.fst) : False

theorem Flypitch.fol.complete_maximal_extension_of_consis {L : Language} {T : Theory L} {hT : is_consistent T} : is_complete ↑(maximal_extension T hT).fst

noncomputable def Flypitch.fol.completion_of_consis {L : Language} (T : Theory L) (h_consis : is_consistent T) : (T' : TheoryOver T h_consis) ×' is_complete ↑T'

Given a consistent theory, return a complete extension of it.

Equations

• Flypitch.fol.completion_of_consis T h_consis = ⟨(Flypitch.fol.maximal_extension T h_consis).fst, ⋯⟩