Barwise Compactness Data

This file defines BarwiseCompactnessData, the literature-faithful interface for the Barwise compactness theorem (Theorem 3.1.3 of [KK04], Theorem 5.6 of [Bar75]). Unlike the project's existing FiniteCompactFragment.compact field (which demands unrestricted finite-subset compactness on arbitrary theories), this structure uses:

• A-coded subtheories via a Code type with a decode map, capturing the standard notion "T₀ ∈ A" (subtheories that are elements of the admissible set) without requiring a full formalization of KP set theory.
• Σ₁-on-A definability as a predicate on theories, restricting compactness to the Σ₁-definable theories (rather than all theories in the fragment).

Design Notes

The standard Barwise compactness theorem:

Let A be a countable admissible set. If Γ is Σ₁-on-A and Γ ⊆ L_A, and every T₀ ∈ A with T₀ ⊆ Γ has a model, then Γ has a model.

The key internality: "T₀ ∈ A" means the subtheory is literally an element of the admissible set, not just an externally-finite subset. This internality is what lets the proof use Σ-reflection and Δ₀-separation inside A. A bare isAFinite : Set Sentenceω → Prop predicate would lose that structure; hence we use a Code type with decode.

The barwiseHeight field represents o(A), the ordinal of the admissible set. No lower bound is imposed: the case o(A) = ω (A = HF, hereditarily finite sets) is the structurally important case where A-coded = finite and L_A = first-order logic (classical compactness as a special case of Barwise compactness). (AdmissibleFragmentCore.height likewise carries no lower bound.)

The isSigma1 predicate is currently abstract (Prop-valued). A future refinement could carry witness data (the Σ formula defining the theory in (A, ∈)), but that would require formalizing the Σ/Δ₀ formula hierarchy for the ∈-language, which is a separate substantial project.

References

• [KK04] Keisler–Knight, "Barwise: Infinitary Logic and Admissible Sets" (2004)
• [Bar75] Barwise, Admissible Sets and Structures (1975), Ch. III, V
• [Bar69] Barwise, "Infinitary Logic and Admissible Sets" (JSL 1969)

structure FirstOrder.Language.BarwiseCompactnessData (L : Language) extends L.AdmissibleFragmentCore : Type (max (max 1 u) v)

The data for a literature-faithful statement of the Barwise compactness theorem. Extends AdmissibleFragmentCore with A-coded subtheories and Σ₁-on-A definability.

The Code type represents elements of the admissible set A that are sets of sentences (the "A-coded subtheories" / "A-finite subtheories"). The decode map sends a code to its actual set of sentences. The compact field then says: if Γ is Σ₁-on-A and every A-coded subtheory of Γ has a model, then Γ has a model.

• formulas : Set L.Sentenceω
• height : Ordinal.{0}
• closed_neg (φ : L.Sentenceω) : φ ∈ self.formulas → BoundedFormulaω.not φ ∈ self.formulas
• closed_imp (φ ψ : L.Sentenceω) : φ ∈ self.formulas → ψ ∈ self.formulas → BoundedFormulaω.imp φ ψ ∈ self.formulas
• closed_iInf (φs : ℕ → L.Sentenceω) : (∀ (k : ℕ), φs k ∈ self.formulas) → BoundedFormulaω.iInf φs ∈ self.formulas
• closed_iSup (φs : ℕ → L.Sentenceω) : (∀ (k : ℕ), φs k ∈ self.formulas) → BoundedFormulaω.iSup φs ∈ self.formulas
• closed_quantifier_instance (φ : L.Formulaω (Fin 1)) (t : L.Term Empty) : (BoundedFormulaω.relabel Sum.inr φ).ex ∈ self.formulas → (BoundedFormulaω.subst φ fun (x : Fin 1) => t) ∈ self.formulas
• falsum_mem : BoundedFormulaω.falsum ∈ self.formulas
• closed_imp_left (φ ψ : L.Sentenceω) : BoundedFormulaω.imp φ ψ ∈ self.formulas → φ ∈ self.formulas
• closed_imp_right (φ ψ : L.Sentenceω) : BoundedFormulaω.imp φ ψ ∈ self.formulas → ψ ∈ self.formulas
• closed_iInf_component (φs : ℕ → L.Sentenceω) (k : ℕ) : BoundedFormulaω.iInf φs ∈ self.formulas → φs k ∈ self.formulas
• closed_iSup_component (φs : ℕ → L.Sentenceω) (k : ℕ) : BoundedFormulaω.iSup φs ∈ self.formulas → φs k ∈ self.formulas
• Code : Type

  Type of codes for subtheories in A (the "A-coded" / "A-finite" sets).

• decode : self.Code → Set L.Sentenceω

  Decode a code to the set of sentences it represents.

• decode_sub_formulas (c : self.Code) : self.decode c ⊆ self.formulas

  Every decoded set is contained in the fragment.

• barwiseHeight : Ordinal.{0}

  The ordinal height o(A) of the admissible set. No lower bound is imposed: o(A) = ω (the HF case) is the structurally important special case where A-coded = finite and L_A = first-order logic.

• finite_has_code (S : Set L.Sentenceω) : S.Finite → S ⊆ self.formulas → ∃ (c : self.Code), self.decode c = S

  Every finite subset of the fragment has an A-code. This holds for all admissible sets A ⊇ ω (including HF, L(ω₁^CK), etc.).

• isSigma1 : Set L.Sentenceω → Prop

  Sigma-1-on-A definability predicate for theories. A set of sentences is Sigma-1-on-A if it is definable in (A, membership) by a Sigma formula. Currently abstract (Prop-valued); a future refinement could carry the defining Sigma formula as witness data.

• compact (Γ : Set L.Sentenceω) : self.isSigma1 Γ → Γ ⊆ self.formulas → (∀ (c : self.Code), self.decode c ⊆ Γ → ∃ (M : Type) (x : L.Structure M), Theoryω.Model (self.decode c) M) → ∃ (M : Type) (x : L.Structure M), Theoryω.Model Γ M

  Barwise compactness: for Σ₁-on-A theories contained in the fragment, if every A-coded subtheory has a model, then the whole theory has a model. This is the standard Barwise compactness theorem (Thm 3.1.3, [KK04]; Thm 5.6, [Bar75]).

theorem FirstOrder.Language.barwise_compactness_of_data {L : Language} (B : L.BarwiseCompactnessData) {Γ : Set L.Sentenceω} (hSigma : B.isSigma1 Γ) (hΓ : Γ ⊆ B.formulas) (hfin : ∀ (c : B.Code), B.decode c ⊆ Γ → ∃ (M : Type) (x : L.Structure M), Theoryω.Model (B.decode c) M) : ∃ (M : Type) (x : L.Structure M), Theoryω.Model Γ M

Barwise compactness theorem, stated as a standalone theorem using BarwiseCompactnessData.