The HF fragment (issue #18)

L_HF = L_ωω: the first-order image inside Lω₁ω, as an honest admissible fragment, plus its compactness theorem derived from Mathlib.

This is the regression oracle for the interface. Any proposed change to AdmissibleFragment must keep all four conditions:

1. the underlying formulas are exactly the toLω-image (sentence_slice_hfFragment);
2. coded families reduce to finite ones — here, to none at all;
3. the compactness theorem is finitaryFragment_compact;
4. no adapter widens it back to all of Lω₁ω.

Where the emptiness lives. hfFamily.IsFamilyCode is False. Not the index type's cardinality, and not einf's ⊤-padding, which is legitimate for a real infinitary code. The forbidden move is granting the certificate to a finite code and using padding to manufacture a primitive iInf.

Universes. The syntax layer and finitaryFragment_compactIn are universe-general; the latter returns Mathlib's canonical model in Type (max u v). The compatibility theorem finitaryFragment_compact retains its published universe-zero result type.

Not built on the legacy structures. AdmissibleFragmentCore.hf := Set.univ is a quarantined placeholder; nothing here uses it, and nothing here may be proved from it.

def FirstOrder.Language.hfSet (L : Language) : Set ((n : ℕ) × L.BoundedFormulaω Empty n)

The all-arity first-order image: every formula containing no infinitary node.

Equations

• L.hfSet = {p : (n : ℕ) × L.BoundedFormulaω Empty n | p.snd.IsFirstOrder}

@[simp]

theorem FirstOrder.Language.mem_hfSet_iff {L : Language} {n : ℕ} {φ : L.BoundedFormulaω Empty n} : ⟨n, φ⟩ ∈ L.hfSet ↔ φ.IsFirstOrder

def FirstOrder.Language.hfFragment (L : Language) : L.Fragment

The HF fragment. Each field is now one appeal to the first-order-image API: three structural equations and the two negative facts. Compare the five hand-rolled constructor inversions this replaces.

Equations

• L.hfFragment = { toSet := L.hfSet, imp_left_mem := ⋯, imp_right_mem := ⋯, all_mem := ⋯, iInf_mem := ⋯, iSup_mem := ⋯ }

def FirstOrder.Language.finitaryFragment (L : Language) : Set L.Sentenceω

The finitary fragment: the image of first-order syntax in Lω₁ω. This is L_HF = L_ωω.

Equations

• L.finitaryFragment = Set.range FirstOrder.Language.Sentence.toLω

theorem FirstOrder.Language.mem_finitaryFragment_iff {L : Language} {φ : L.Sentenceω} : φ ∈ L.finitaryFragment ↔ ∃ (φ₀ : L.Sentence), φ₀.toLω = φ

theorem FirstOrder.Language.sentence_slice_hfFragment (L : Language) : {φ : L.Sentenceω | ⟨0, φ⟩ ∈ L.hfFragment} = L.finitaryFragment

The oracle, condition 1. The sentence slice of hfFragment is exactly finitaryFragment. Any proposed AdmissibleFragment whose HF instance fails this is wrong.

Both sides are universe-general.

def FirstOrder.Language.foTheory {L : Language} (T : Set L.Sentenceω) : L.Theory

The full preimage theory — every first-order sentence whose image lies in T, not one chosen representative per member. Choosing representatives would need Classical.choice and would make the model correspondence direction-sensitive.

Equations

• FirstOrder.Language.foTheory T = {φ₀ : L.Sentence | φ₀.toLω ∈ T}

theorem FirstOrder.Language.model_foTheory_iff {L : Language} {T : Set L.Sentenceω} (hT : T ⊆ L.finitaryFragment) (M : Type w) [L.Structure M] [Nonempty M] : M ⊨ foTheory T ↔ Theoryω.Model T M

Model correspondence. For a theory inside the finitary fragment, models of the preimage theory are exactly models of the original.

theorem FirstOrder.Language.finitaryFragment_compactIn {L : Language} {T : L.Theoryω} (hT : T ⊆ L.finitaryFragment) (hfin : T.IsFinitelySatisfiableIn) : T.IsSatisfiableIn

Universe-general compactness for the finitary fragment, derived from Mathlib's first-order compactness.

No compact field is consulted: the infinitary finite-satisfiability hypothesis is pushed through toLω to the preimage theory, Mathlib supplies its canonical model in Type (max u v), and the correspondence carries it back. Finite-subtheory witnesses may live in any fixed Type w; their universe is independent of the output universe.

theorem FirstOrder.Language.finitaryFragment_compact {L : Language} {T : L.Theoryω} (hT : T ⊆ L.finitaryFragment) (hfin : T.IsFinitelySatisfiable) : T.IsSatisfiable

Universe-zero compatibility endpoint. This retains the published result type while the underlying first-order argument is universe-general; use finitaryFragment_compactIn when the language or resulting carrier lives above universe zero.

Gate 4 — the HF oracle

For HF the certificate is empty, so CodedFamily is uninhabited and the upward-closure fields of any AdmissibleFragment over it are vacuous. Note where the emptiness lives: in IsFamilyCode, not in the index type's cardinality and not in einf's padding.

theorem FirstOrder.Language.isEmpty_codedFamily_hf {L : Language} {n : ℕ} : IsEmpty (CodedFamily L.hfFamily n)

Gate 4. CodedFamily over HF is uninhabited.

Stated over hfFamily, the family-layer HF presentation, so the syntax consumers of HF depend on no presentation carrying theory decoding or Sigma1. The emptiness comes solely from IsFamilyCode := False.

theorem FirstOrder.Language.hf_coded_closure_vacuous {L : Language} {n : ℕ} (S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) (F : CodedFamily L.hfFamily n) : (∀ (i : L.hfFamily.Index F.code), ⟨n, F.decode i⟩ ∈ S) → ⟨n, codedIInf F⟩ ∈ S

Consequently every upward-closure obligation over HF is vacuous, for any target set.

Step 4 — the honest HF instance

Essentially a structure literal: the base is hfFragment, and both upward fields are closed by certificate absurdity. That it is nearly definitional is the signal that the signature is right.

def FirstOrder.Language.hfAdmissibleFragment (L : Language) : AdmissibleFragment L.hfFamily

The HF admissible fragment. No adapter, no widening.

Equations

• L.hfAdmissibleFragment = { toFragment := L.hfFragment, iInf_coded_mem := ⋯, iSup_coded_mem := ⋯ }

theorem FirstOrder.Language.hfAdmissibleFragment_toFragment (L : Language) : L.hfAdmissibleFragment.toFragment = L.hfFragment

Oracle condition 1, at the interface level. The HF admissible fragment's underlying Fragment is exactly hfFragment, whose sentence slice is finitaryFragment.

The universe boundary

The structures are language-indexed and universe-polymorphic: FamilyPresentation L for L : Language.{u, v}, so FamilyPresentation L[[J]] is well-formed for an arbitrary parameter type J. The probes below record that, at the signature level only — nothing here claims a presentation for L lifts to one for L[[J]].

The low-level semantic boundary is now explicit: Theoryω.IsSatisfiableIn selects the carrier universe, and finitaryFragment_compactIn works for any language. The ambient presentation API still concludes the published universe-zero Theoryω.IsSatisfiable; that remaining boundary is enforced separately by scripts/check_admissible_universes.lean.

Write the probe results as Type _, not Type: bare Type means Type 0, and that constraint propagates backward onto the presentation argument.