Barwise Compactness and Completeness

This file states the Barwise compactness theorem and Barwise completeness II for admissible fragments of Lω₁ω.

Main Results

• barwise_compactness: If every A-finite subset of a theory T (within an admissible fragment A) has a model, then T itself has a model.
• barwise_completeness_II: A theory in an admissible fragment that is consistent (in the proof-theoretic sense) has a model.

References

• [KK04], §3.1
• [Bar75]

theorem FirstOrder.Language.barwise_compactness {L : Language} (A : L.AdmissibleFragment) {T : Set L.Sentenceω} (hT : T ⊆ A.formulas) (hfin : ∀ (S : Set L.Sentenceω), A.AFinite S → S ⊆ T → ∃ (M : Type) (x : L.Structure M), Theoryω.Model S M) : ∃ (M : Type) (x : L.Structure M), Theoryω.Model T M

Barwise Compactness Theorem (KK04 Theorem 3.1.3).

If every A-finite subset of a theory T (contained in an admissible fragment A) has a model, then T itself has a model.

This is a far-reaching generalization of the classical compactness theorem. While full first-order compactness fails for Lω₁ω, this restricted form holds for theories within admissible fragments.

theorem FirstOrder.Language.barwise_completeness_II {L : Language} [Countable ((l : ℕ) × L.Functions l)] [Countable ((l : ℕ) × L.Relations l)] (A : L.AdmissibleFragment) {T : Set L.Sentenceω} (_hT : T ⊆ A.formulas) (hT_countable : T.Countable) (hcons : ∃ (C : L.ConsistencyPropertyEq), T ∈ C.sets) : ∃ (M : Type u) (x : L.Structure M) (_ : Countable M), Theoryω.Model T M

Barwise Completeness II (KK04 Theorem 3.1.2).

A countable theory in an admissible fragment of a countable language that is consistent (with equality axioms) has a countable model.

Here "consistent" is stated schematically as membership in some consistency property restricted to the fragment. The full statement requires a proof system for the admissible fragment, which we do not formalize.