Completeness of first-order logic

This file formalizes the completeness theorem (also referred as Gödel's completeness theorem) of first-order logic.

The proof mainly follows flypitch:

1. We first prove that any theory can be extended with Henkin constants and Henkin axioms while keeping its consistency (FormulaSet.henkinStep).
2. We then prove that starting from a consistent theory, extends it with Henkin constants ω times creates a consistent theory that satisfies Henkin property (FormulaSet.henkinize).
3. We show the Lindenbaum's theorem: any consistent theory can be extended to a consistent, complete theory (FormulaSet.lindenbaum).
4. Finally we show that a consistent, complete theory satisfying Henkin property is satisfiable by its syntactic terms (FormulaSet.TermModel).

This file collects the main results only; the details are decomposed into files under Completeness folder (Language.lean, Henkin.lean, Lindenbaum.lean and TermModel.lean).

References

• flypitch. https://github.com/flypitch/flypitch

theorem FirstOrder.Language.Satisfiable.of_consistent {n : ℕ} {L : Language} {Γ : L.FormulaSet n} : Consistent Γ → Satisfiable.{u_1} Γ

theorem FirstOrder.Language.consistent_iff_satisfiable {n : ℕ} {L : Language} {Γ : L.FormulaSet n} : Consistent Γ ↔ Satisfiable.{u_1} Γ

theorem FirstOrder.Language.completeness {n : ℕ} {L : Language} {Γ : L.FormulaSet n} {p : L.Formula n} : Γ ⊨ p → Γ ⊢ p

Completeness theorem.

theorem FirstOrder.Language.provable_iff_entails {n : ℕ} {L : Language} {Γ : L.FormulaSet n} {p : L.Formula n} : Γ ⊢ p ↔ Γ ⊨ p

theorem FirstOrder.Language.Entails.compactness {n : ℕ} {L : Language} {Γ : L.FormulaSet n} {p : L.Formula n} : Γ ⊨ p → ∃ Δ ⊆ Γ, Set.Finite Δ ∧ Δ ⊨ p

theorem FirstOrder.Language.Satisfiable.compactness {n : ℕ} {L : Language} {Γ : L.FormulaSet n} : Satisfiable.{u} Γ ↔ ∀ Δ ⊆ Γ, Set.Finite Δ → Satisfiable.{u} Δ

Compactness theorem.

theorem FirstOrder.Language.Theory.complete_iff_elementary_equivalent {L : Language} {T : L.Theory} : Complete T ↔ ∀ (M : T.Model) (N : T.Model), M.toStructure ≃ᴱ N.toStructure