Compactness and Completeness for Admissible Fragments

This file provides compactness and completeness theorems for FiniteCompactFragment, which uses finite-subset compactness (the HF-style axiom baked into the compact field).

Important: barwise_compactness here is a direct wrapper around FiniteCompactFragment.compact, which assumes compactness for ALL theories with ordinary finite satisfiability. This is stronger than the standard Barwise compactness theorem (Theorem 3.1.3 of [KK04]), which restricts to Σ₁-on-A theories with A-finite subsets. See BarwiseCompactnessData (in Barwise/Data.lean) for the literature-faithful version.

Main Results

• barwise_compactness: If every finite subset of a theory T (within an admissible fragment A) has a model, then T itself has a model. (Wrapper around A.compact; stronger than the standard Barwise theorem.)
• 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], Ch. III

theorem FirstOrder.Language.barwise_compactness {L : Language} (A : L.FiniteCompactFragment) {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

Finite-subset compactness (wrapper around FiniteCompactFragment.compact).

If every finite subset of a theory T (contained in an admissible fragment A) has a model, then T itself has a model. This is a direct application of the compact field, which assumes unrestricted finite-subset compactness.

Naming note: despite its name, this theorem is strictly stronger than the standard Barwise Compactness Theorem (KK04 Theorem 3.1.3), which restricts to Σ₁-on-A theories and A-finite subsets (where "A-finite" = ∈ A, not ordinary finiteness). The standard theorem is available via BarwiseCompactnessData.

theorem FirstOrder.Language.barwise_completeness_II {L : Language} [Countable ((l : ℕ) × L.Functions l)] [Countable ((l : ℕ) × L.Relations l)] (A : L.FiniteCompactFragment) {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.