NF weak partition development: Flypitch4.Completeness.

satisfied_of_provable

Soundness: provability implies semantic consequence.

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

completeness_for_inconsistent_theories

For an inconsistent theory, provability and semantic entailment coincide trivially.

theorem NFChoice.Fol.completeness_for_inconsistent_theories {L : Language} (T : SentTheory L) (ψ : sentence L) (h_inconsis : ¬T.isConsistent) : T.sprovable ψ ↔ ssatisfied T ψ

model_existence

T is consistent iff there is a nonempty model of T.

theorem NFChoice.Fol.model_existence {L : Language} (T : SentTheory L) : T.isConsistent ↔ ∃ (M : Structure L), Nonempty M.carrier ∧ allRealizeSentence M T

nonempty_model_of_consis

A consistent theory has a nonempty model.

noncomputable def NFChoice.Fol.nonemptyModelOfConsis {L : Language} {T : SentTheory L} (hT : T.isConsistent) : (M : Structure L) ×' Nonempty M.carrier ∧ allRealizeSentence M T

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

Equations

• NFChoice.Fol.nonemptyModelOfConsis hT = ⟨⋯.choose, ⋯⟩

completeness

The Gödel completeness theorem: T ⊢ₛ' ψ ↔ ssatisfied T ψ.

theorem NFChoice.Fol.completeness {L : Language} (T : SentTheory L) (ψ : sentence L) : T.sprovable ψ ↔ ssatisfied T ψ

compactness

Semantic compactness: T ⊨ f iff some finite subset of T semantically entails f.

theorem NFChoice.Fol.compactness {L : Language} {T : SentTheory L} {f : sentence L} : ssatisfied T f ↔ ∃ (fs : Finset (sentence L)), ssatisfied (↑ fs) f ∧ ↑ fs ⊆ T