Admissible fragment from a bare compactness hypothesis

admissibleFragmentOfUniv constructs an FiniteCompactFragment L with formulas := Set.univ from a bare compactness hypothesis. All closure fields (from AdmissibleFragmentCore) are trivial because Set.univ is trivially closed under everything; the compact field is forwarded from the input.

This is a packaging constructor, not a substantive theorem: the hard content (the finite-subset compactness property) is assumed, not derived. Note that the resulting FiniteCompactFragment.compact is the HF-style finite-subset compactness, which is stronger than the standard Barwise compactness theorem. See BarwiseCompactnessData for the literature-faithful version.

noncomputable def FirstOrder.Language.admissibleFragmentOfUniv {L : Language} (height : Ordinal.{0}) (h_height : Ordinal.omega0 < height) (hCompact : ∀ (S : Set L.Sentenceω), (∀ (F : Set L.Sentenceω), F.Finite → F ⊆ S → ∃ (M : Type) (x : L.Structure M), Theoryω.Model F M) → ∃ (M : Type) (x : L.Structure M), Theoryω.Model S M) : L.FiniteCompactFragment

An admissible fragment on the full universe of sentences, built from a bare compactness hypothesis. All closure fields are trivial because formulas is Set.univ. The height is taken as a parameter (any ordinal > ω suffices).

This is a packaging constructor: the hard content (compactness) is assumed as hCompact, not derived from any prior fragment or admissibility argument. Callers that have a FullBarwiseFragment L can supply B.height and B.height_gt_omega for the ordinal parameters.

Equations

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

@[simp]

theorem FirstOrder.Language.admissibleFragmentOfUniv_formulas {L : Language} {height : Ordinal.{0}} {h_height : Ordinal.omega0 < height} {hCompact : ∀ (S : Set L.Sentenceω), (∀ (F : Set L.Sentenceω), F.Finite → F ⊆ S → ∃ (M : Type) (x : L.Structure M), Theoryω.Model F M) → ∃ (M : Type) (x : L.Structure M), Theoryω.Model S M} : (admissibleFragmentOfUniv height h_height hCompact).formulas = Set.univ