Admissible Fragments

This file defines an abstract notion of admissible fragment of Lω₁ω, providing the interface needed for Barwise compactness and completeness without formalizing the full theory of admissible sets or KP set theory.

Main Definitions

• AdmissibleFragment: An abstract admissible fragment, given as a set of Lω₁ω sentences closed under subformulas and Boolean/quantifier operations.
• AdmissibleFragment.AFinite: A set is A-finite if it is a finite subset of the fragment's formulas.

References

• [KK04], §3
• [Bar75]

structure FirstOrder.Language.AdmissibleFragment (L : Language) : Type (max (max u (u_1 + 1)) v)

An abstract admissible fragment of Lω₁ω.

This captures the essential closure properties of an admissible set's intersection with the formulas of Lω₁ω, without requiring a full formalization of KP set theory or admissible sets.

The height ordinal represents the ordinal height of the admissible set (o(A)), which bounds the complexity of formulas in the fragment.

• formulas : Set L.Sentenceω

  The set of sentences belonging to this fragment.

• height : Ordinal.{u_1}

  The ordinal height of the admissible set.

• height_gt_omega : Ordinal.omega0 < self.height

  The height is > ω.

• closed_neg (φ : L.Sentenceω) : φ ∈ self.formulas → BoundedFormulaω.not φ ∈ self.formulas

  Closure under negation.

• closed_imp (φ ψ : L.Sentenceω) : φ ∈ self.formulas → ψ ∈ self.formulas → BoundedFormulaω.imp φ ψ ∈ self.formulas

  Closure under implication.

• closed_iInf (φs : ℕ → L.Sentenceω) : (∀ (k : ℕ), φs k ∈ self.formulas) → BoundedFormulaω.iInf φs ∈ self.formulas

  Closure under countable conjunction (for families in the fragment).

• closed_iSup (φs : ℕ → L.Sentenceω) : (∀ (k : ℕ), φs k ∈ self.formulas) → BoundedFormulaω.iSup φs ∈ self.formulas

  Closure under countable disjunction (for families in the fragment).

• 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

  Closure under quantifier instances: if an existential sentence (φ.relabel Sum.inr).ex is in the fragment, then the substitution instance φ.subst (fun _ => t) is also in the fragment for any closed term t. This ensures Henkin witnesses stay within the fragment and is needed for the consistency property in Barwise compactness.

• falsum_mem : BoundedFormulaω.falsum ∈ self.formulas

  Falsum belongs to the fragment.

• closed_imp_left (φ ψ : L.Sentenceω) : BoundedFormulaω.imp φ ψ ∈ self.formulas → φ ∈ self.formulas

  Backward closure: implication left component.

• closed_imp_right (φ ψ : L.Sentenceω) : BoundedFormulaω.imp φ ψ ∈ self.formulas → ψ ∈ self.formulas

  Backward closure: implication right component.

• closed_iInf_component (φs : ℕ → L.Sentenceω) (k : ℕ) : BoundedFormulaω.iInf φs ∈ self.formulas → φs k ∈ self.formulas

  Backward closure: conjunction components.

• closed_iSup_component (φs : ℕ → L.Sentenceω) (k : ℕ) : BoundedFormulaω.iSup φs ∈ self.formulas → φs k ∈ self.formulas

  Backward closure: disjunction components.

• 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

  Compactness principle (Σ₁-reflection in the underlying admissible set). If every A-finite subset of S ⊆ formulas has a model, then S has a model. This is the key set-theoretic property of admissible fragments that cannot be derived from closure properties alone. See [Bar75].

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

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

Equations

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