Admissible Fragment with Compact Field

Extends AdmissibleFragmentCore with a finite-subset compactness axiom. This is the HF-style compactness principle (stronger than the standard Barwise theorem). See BarwiseCompactnessData for the literature-faithful version.

Retained for backward compatibility with existing consumers.

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

An abstract admissible fragment of Lω₁ω, extending AdmissibleFragmentCore with a finite-subset compactness axiom.

Important: the compact field uses ordinary finite satisfiability, which matches the Barwise compactness theorem only for the case A = HF (hereditarily finite sets, i.e., first-order logic). For Lω₁ω with a general admissible set, the standard Barwise theorem restricts to Σ₁-on-A theories with A-finite subsets (where "A-finite" = ∈ A, not ordinary finiteness). See BarwiseCompactnessData for the literature-faithful version.

This structure is retained for backward compatibility with existing consumers (barwise_compactness, ConsistencyBridge, EMRealization).

• 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
• height_gt_omega : Ordinal.omega0 < self.height

  The height is > ω. This constraint is specific to the legacy compact wrapper (not imposed by AdmissibleFragmentCore). It excludes the HF case but is needed by some downstream consumers (e.g., admissibleFragmentOfUniv).

• compact (S : Set L.Sentenceω) : S ⊆ self.formulas → (∀ F ⊆ self.formulas, F.Finite → F ⊆ S → ∃ (M : Type) (x : L.Structure M), Theoryω.Model F M) → ∃ (M : Type) (x : L.Structure M), Theoryω.Model S M

  Finite-subset compactness (stronger than the standard Barwise theorem). If every finite subset of S ⊆ formulas has a model, then S has a model. This is the HF-style compactness principle; the standard Barwise compactness restricts to Σ₁-on-A theories and A-finite subsets.

def FirstOrder.Language.FiniteCompactFragment.AFinite {L : Language} (A : L.FiniteCompactFragment) (S : Set L.Sentenceω) : Prop

A set of sentences is A-finite (finite and contained in the fragment).

Note: this uses ordinary finiteness, matching the HF case. For the standard Barwise notion "T₀ ∈ A" (which includes hyperarithmetical sets for A = L(ω₁^CK)), see BarwiseCompactnessData.isAFinite.

Equations

• A.AFinite S = (S ⊆ A.formulas ∧ S.Finite)