Admissible Fragment Core: Closure Properties

The syntactic closure properties of an admissible fragment L_A, capturing the closure of an admissible set's intersection with the formulas of Lω₁ω. This is the pure interface layer — no compactness principle, no model-existence claim. Every consumer that needs only closure properties (proof system, soundness, Nadel bound) can use this layer directly.

References

• [KK04], §3
• [Bar75], Ch. III

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

The syntactic closure properties of an admissible fragment of Lω₁ω.

This captures the closure of an admissible set's intersection with the formulas of Lω₁ω (the "admissible fragment" L_A), without including the compactness principle. Every consumer that needs only closure properties (proof system, soundness, Nadel bound) can use this layer directly.

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.{0}

  The ordinal height of the admissible set. No lower bound is imposed at this layer: the HF case (o(A) = ω) is structurally important and should not be excluded. See FiniteCompactFragment.height_gt_omega for the stronger constraint used by the legacy compact wrapper.

• 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.

def FirstOrder.Language.AdmissibleFragmentCore.hf {L : Language} : L.AdmissibleFragmentCore

LEGACY PLACEHOLDER — not the HF fragment. Its formula set is Set.univ, i.e. all of Lω₁ω, whereas the HF fragment should be L_ωω (finitary first-order syntax). It survives only as a smoke test that AdmissibleFragmentCore admits some height-ω instance.

Do not read this as "the HF case is covered". The honest finitary specialization — with A-finite = finite and compactness derived from Mathlib's first-order compactness — is issue #18. See also the finitaryFragment design sketched there.

Equations

• One or more equations did not get rendered due to their size.