NF weak partition development: Flypitch4.Completion.

Helper lemmas at the sentence level

theorem NFChoice.Fol.saxm' {L : Language} {T : SentTheory L} {ψ : sentence L} (h : ψ ∈ T) : T.sprovable ψ

A sentence-level axiom rule: if ψ ∈ T (as a SentTheory), then T ⊢ₛ' ψ

theorem NFChoice.Fol.sweakening' {L : Language} {T T' : SentTheory L} (h_sub : T ⊆ T') {ψ : sentence L} (h : T.sprovable ψ) : T'.sprovable ψ

Sentence-level weakening for sprovable

theorem NFChoice.Fol.snot_and_self'' {L : Language} {T : SentTheory L} {ψ : sentence L} (H₁ : T.sprovable ψ) (H₂ : T.sprovable (bdNot ψ)) : T.sprovable bd_falsum

snot_and_self: from T ⊢ₛ' ψ and T ⊢ₛ' ∼ᵇψ, derive T ⊢ₛ' bd_falsum

theorem NFChoice.Fol.sfalsumE {L : Language} {T : SentTheory L} {ψ : sentence L} (h : T.sprovable bd_falsum) : T.sprovable ψ

sfalsumE: from T ⊢ₛ' bd_falsum derive T ⊢ₛ' ψ (ex falso)

theorem NFChoice.Fol.simpI {L : Language} {T : SentTheory L} {ψ ϕ : sentence L} (h : T.sprovable ψ) : (insert ϕ T).sprovable ψ

Sentence-level simpI: T ⊢ₛ' ψ → insert ϕ T ⊢ₛ' ψ

Helper: (insert ψ T).fst = insert ψ.fst T.fst

consis_not_of_not_provable and inconsis_not_of_provable

theorem NFChoice.Fol.consis_not_of_not_provable {L : Language} {T : SentTheory L} {f : sentence L} (h : ¬T.sprovable f) : (insert (bdNot f) T).isConsistent

If T ⊬ₛ' f, then T ∪ {∼ᵇf} is consistent

theorem NFChoice.Fol.inconsis_not_of_provable {L : Language} {T : SentTheory L} {f : sentence L} (H : T.sprovable f) : ¬(insert (bdNot f) T).isConsistent

If T ⊢ₛ' f, then T ∪ {∼ᵇf} is inconsistent

theorem NFChoice.Fol.provable_of_inconsis_not {L : Language} {T : SentTheory L} {f : sentence L} (h : ¬(insert (bdNot f) T).isConsistent) : T.sprovable f

If T ∪ {∼ᵇf} is inconsistent, then T ⊢ₛ' f

can_extend: one of T ∪ {ψ} or T ∪ {∼ᵇψ} is consistent

theorem NFChoice.Fol.can_extend {L : Language} (T : SentTheory L) (ψ : sentence L) (h : T.isConsistent) : (insert ψ T).isConsistent ∨ (insert (bdNot ψ) T).isConsistent

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

Theory_over: the poset of consistent extensions of T

def NFChoice.Fol.TheoryOver {L : Language} (T : SentTheory L) (_hT : T.isConsistent) : Type u

Theory_over T hT: the subtype of SentTheory L consisting of consistent theories ⊇ T

Equations

• NFChoice.Fol.TheoryOver T _hT = { T' : NFChoice.Fol.SentTheory L // T ⊆ T' ∧ T'.isConsistent }

def NFChoice.Fol.overSelf {L : Language} (T : SentTheory L) (hT : T.isConsistent) : TheoryOver T hT

T itself is a Theory_over T hT

Equations

• NFChoice.Fol.overSelf T hT = ⟨T, ⋯⟩

def NFChoice.Fol.TheoryOverSubset {L : Language} {T : SentTheory L} {hT : T.isConsistent} : TheoryOver T hT → TheoryOver T hT → Prop

Subset order on Theory_over T hT

Equations

• NFChoice.Fol.TheoryOverSubset T1 T2 = (↑T1 ⊆ ↑T2)

@[instance_reducible]

instance NFChoice.Fol.instHasSubsetTheoryOver {L : Language} {T : SentTheory L} {hT : T.isConsistent} : HasSubset (TheoryOver T hT)

Equations

• NFChoice.Fol.instHasSubsetTheoryOver = { Subset := NFChoice.Fol.TheoryOverSubset }

instance NFChoice.Fol.instNonemptyTheoryOver {L : Language} {T : SentTheory L} {hT : T.isConsistent} : Nonempty (TheoryOver T hT)

consis_limit: the limit of a chain is consistent

theorem NFChoice.Fol.consis_limit {L : Language} {T : SentTheory L} {hT : T.isConsistent} (Ts : Set (TheoryOver T hT)) (h_chain : IsChain TheoryOverSubset Ts) : (T ∪ ⋃₀ (Subtype.val '' Ts)).isConsistent

The union of a chain of consistent extensions of T is consistent

limit_theory: build the limit as a Theory_over

noncomputable def NFChoice.Fol.limitTheory {L : Language} {T : SentTheory L} {hT : T.isConsistent} (Ts : Set (TheoryOver T hT)) (h_chain : IsChain TheoryOverSubset Ts) : (T_lim : TheoryOver T hT) ×' ∀ T' ∈ Ts, ↑T' ⊆ ↑T_lim

Given a chain of consistent extensions, their union is a consistent extension

Equations

• NFChoice.Fol.limitTheory Ts h_chain = ⟨⟨T ∪ ⋃₀ (Subtype.val '' Ts), ⋯⟩, ⋯⟩

can_use_zorn

theorem NFChoice.Fol.can_use_zorn {L : Language} {T : SentTheory L} {hT : T.isConsistent} : (∀ (c : Set (TheoryOver T hT)), IsChain TheoryOverSubset c → ∃ (ub : TheoryOver T hT), ∀ a ∈ c, a ⊆ ub) ∧ ∀ (a b c : TheoryOver T hT), TheoryOverSubset a b → TheoryOverSubset b c → TheoryOverSubset a c

The poset of theories over T satisfies Zorn's hypotheses

maximal_extension

noncomputable def NFChoice.Fol.maximalExtension {L : Language} (T : SentTheory L) (hT : T.isConsistent) : (T_max : TheoryOver T hT) ×' ∀ (T' : TheoryOver T hT), T_max ⊆ T' → T' ⊆ T_max

Given a consistent theory T, there is a maximal consistent extension of T

Equations

• NFChoice.Fol.maximalExtension T hT = ⟨⋯.choose, ⋯⟩

cannot_extend_maximal_extension

theorem NFChoice.Fol.cannot_extend_maximal_extension {L : Language} {T : SentTheory L} {hT : T.isConsistent} (T_max' : (T_max : TheoryOver T hT) ×' ∀ (T' : TheoryOver T hT), T_max ⊆ T' → T' ⊆ T_max) (ψ : sentence L) (H : (insert ψ ↑T_max'.fst).isConsistent) (H1 : ψ ∉ ↑T_max'.fst) : False

A maximal extension cannot be consistently extended by any new sentence

is_complete for SentTheory

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

A SentTheory is complete if it is consistent and every sentence or its negation is in it

Equations

• T.isComplete = (T.isConsistent ∧ ∀ (ψ : NFChoice.Fol.sentence L), ψ ∈ T ∨ NFChoice.Fol.bdNot ψ ∈ T)

complete_maximal_extension_of_consis

theorem NFChoice.Fol.complete_maximal_extension_of_consis {L : Language} {T : SentTheory L} {hT : T.isConsistent} : (↑(maximalExtension T hT).fst).isComplete

The maximal extension of a consistent theory is complete

completion_of_consis

noncomputable def NFChoice.Fol.completionOfConsis {L : Language} (T : SentTheory L) (h_consis : T.isConsistent) : (T' : TheoryOver T h_consis) ×' (↑T').isComplete

Every consistent theory has a complete extension

Equations

• NFChoice.Fol.completionOfConsis T h_consis = ⟨(NFChoice.Fol.maximalExtension T h_consis).fst, ⋯⟩