The honest HF ambient instance (issue #19A)

Element := ℕ under Ackermann membership. Sentence codes are the enc-image of the finitary sentences, theory codes are exactly the finite sets of sentence codes, and pairing and union are ordinary arithmetic. The four kinds overlap, which is correct: in HF every code is a number.

A-finiteness is not plain finiteness

Theory codes are built from finitary sentence codes, so a finite theory containing an infinitary sentence is not an element of HF. The characterization is hfAmbient_aFinite_iff:

AFinite T ↔ T.Finite ∧ T ⊆ finitaryFragment L

with hfAmbient_aFinite_iff_of_finitary as the consumer-friendly form. Both conjuncts are necessary: encoding arbitrary infinitary sentences into HF is ruled out by the uncountability of L.Sentenceω (docs/admissible-19a-checkpoint.md §1). not_hfAmbient_aFinite_iff_finite exhibits a finite non-A-finite theory rather than merely asserting the distinction.

What injectivity does and does not give

FinitaryCoding stores an injective numbering. Injectivity gives numbering-independence of the decoded range — hence of adequacy and containment, which is hfAmbient_range_indep — but not of Sigma1: two injective numberings can disagree about which theories are c.e. Sigma1 invariance is a separate layer, and holds only against an explicit ComputablyEquivalent witness; see Admissible/Numbering.lean.

Main definitions

• FinitaryCoding: the stored finitary-sentence numbering.
• hfAmbient: the ambient presentation at Element := ℕ.
• hfAmbientKP: its pairing and union, discharged by Ackermann arithmetic.

Main results

• hfAmbient_adequate: the sentence codes decode onto exactly finitaryFragment L.
• hfAmbient_aFinite_iff: the corrected A-finiteness characterization.
• hfAmbient_compact: the assembled regression, with containment discharged internally.

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

The stored coding. Not [Encodable L.Sentence]: an ambient instance is chosen by instance search and gives no invariance between numberings, so the encoding is carried as data. Same lesson as codedIInf_uses_presentation_encoding.

• enc : L.Sentence → ℕ

  The numbering of finitary sentences.

• enc_injective : Function.Injective self.enc

  Injectivity — enough for range-invariance, not enough for Sigma1-invariance.

noncomputable def FirstOrder.Language.hfAmbient {L : Language} (C : L.FinitaryCoding) : L.AmbientPresentation

The honest HF ambient presentation, relative to a stored coding.

noncomputable only because decodeSentence inverts enc by choice; the coding itself is concrete data, which is the point of storing it.

Equations

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

theorem FirstOrder.Language.hfAmbient_toFamilyPresentation {L : Language} (C : L.FinitaryCoding) : (hfAmbient C).toFamilyPresentation = L.hfFamily

The ambient instance and the family-layer HF presentation agree, definitionally.

hfFamily is what the HF syntax consumers (isEmpty_codedFamily_hf, hf_coded_closure_vacuous, hfAdmissibleFragment) are stated over, and this is what ties them to the ambient instance without either one depending on the other's extra layers. It is also independent of the coding C, as it must be: the family layer sees no sentence numbering.

theorem FirstOrder.Language.hfAmbient_decode {L : Language} (C : L.FinitaryCoding) (φ₀ : L.Sentence) (h : (hfAmbient C).IsSentenceCode (C.enc φ₀)) : (hfAmbient C).decodeSentence ⟨C.enc φ₀, h⟩ = φ₀.toLω

Decoding a stored code returns that very sentence — this is where enc_injective is used, and why the coding must be stored rather than assumed.

theorem FirstOrder.Language.hfAmbient_adequate {L : Language} (C : L.FinitaryCoding) : (hfAmbient C).AdequateFor L.finitaryFragment

Adequacy: the HF sentence codes decode onto exactly finitaryFragment L.

theorem FirstOrder.Language.hfAmbient_range_indep {L : Language} (C C' : L.FinitaryCoding) : (hfAmbient C).sentenceRange = (hfAmbient C').sentenceRange

Numbering invariance, stated the only way it can be. The decoded range is finitaryFragment L for every stored coding, so adequacy — and hence containment — does not depend on which numbering was chosen.

What is not claimed is that Sigma1 is numbering-invariant; that needs acceptable / computably equivalent encodings and is the open half of checkpoint §6(a).

The theory layer

Theory codes are the Ackermann codes all of whose members are sentence codes — so, exactly the finite sets of sentence codes. Nat.finite_ackMem gives one direction, Nat.exists_ack_of_finite the other.

theorem FirstOrder.Language.hfAmbient_members_finite {L : Language} (C : L.FinitaryCoding) (a : (hfAmbient C).TheoryCode) : ((hfAmbient C).members a).Finite

The members of a theory code form a finite set of sentence codes.

theorem FirstOrder.Language.hfAmbient_aFinite_iff {L : Language} (C : L.FinitaryCoding) {T : L.Theoryω} : (hfAmbient C).AFinite T ↔ Set.Finite T ∧ T ⊆ L.finitaryFragment

The corrected A-finiteness characterization.

Both conjuncts are necessary. Finiteness comes from Nat.finite_ackMem: an Ackermann code has finitely many bits set. Containment comes from adequacy: the members are sentence codes, and those decode into the finitary fragment and nowhere else.

The global form AFinite T ↔ T.Finite is FALSE here; not_hfAmbient_aFinite_iff_finite exhibits a counterexample.

theorem FirstOrder.Language.hfAmbient_aFinite_iff_of_finitary {L : Language} (C : L.FinitaryCoding) {T : L.Theoryω} (hT : T ⊆ L.finitaryFragment) : (hfAmbient C).AFinite T ↔ Set.Finite T

The consumer-friendly form. Inside the finitary fragment — which is where every HF consumer lives — A-finiteness is ordinary finiteness.

theorem FirstOrder.Language.not_hfAmbient_aFinite_iff_finite {L : Language} (C : L.FinitaryCoding) (φs : ℕ → L.Sentenceω) : ¬((hfAmbient C).AFinite {BoundedFormulaω.iInf φs} ↔ Set.Finite {BoundedFormulaω.iInf φs})

The distinction is real, not cosmetic. A singleton iInf theory is finite yet not A-finite, so AFinite T ↔ T.Finite genuinely fails.

Exhibiting the counterexample is the point: it is what stops that equation from being adopted "for convenience".

KP closure, discharged

Nat.mem_ackPair and Nat.mem_ackUnion are exactly the specification laws WithKP demands, so the HF instance is a structure literal. That it is nearly definitional is the signal that membership was the missing ingredient — the earlier totality-only fields were satisfiable by fun _ _ _ => True and proved nothing.

noncomputable def FirstOrder.Language.hfAmbientKP {L : Language} (C : L.FinitaryCoding) : AmbientPresentation.WithKP L

HF with pairing and union.

Equations

• FirstOrder.Language.hfAmbientKP C = { toAmbientPresentation := FirstOrder.Language.hfAmbient C, pair := Nat.ackPair, mem_pair := ⋯, union := Nat.ackUnion, mem_union := ⋯ }

theorem FirstOrder.Language.hfAmbientKP_toAmbientPresentation {L : Language} (C : L.FinitaryCoding) : (hfAmbientKP C).toAmbientPresentation = hfAmbient C

The KP layer adds laws, not a different presentation.

The assembled regression

The public form takes the presentation's own Sigma1; there is no free Sig parameter and no caller-supplied containment.

theorem FirstOrder.Language.hfAmbient_subset_finitary {L : Language} (C : L.FinitaryCoding) {T : L.Theoryω} (hT : (hfAmbient C).Sigma1 T) : T ⊆ L.finitaryFragment

Containment for HF, derived from adequacy — no manual hypothesis.

Universe-general: only the ambient compactness theorem below is pinned to Language.{0, 0}, because its published interface still concludes the universe-zero Theoryω.IsSatisfiable. The underlying first-order route is universe-general via finitaryFragment_compactIn; no coding fact imposes the restriction.

theorem FirstOrder.Language.hfAmbient_isFinitelySatisfiable {L : Language} (C : L.FinitaryCoding) {T : L.Theoryω} (hT : T ⊆ L.finitaryFragment) (hfin : (hfAmbient C).AFinitelySatisfiable T) : T.IsFinitelySatisfiable

Inside the fragment, the Barwise premise IS ordinary finite satisfiability.

One direction only, and that is the honest shape: a finite subtheory of a finitary theory is itself finitary, so hfAmbient_aFinite_iff's containment conjunct comes for free and every ordinarily finite subtheory is A-finite.

Only this direction is needed, and it is all that holds without further hypotheses.

theorem FirstOrder.Language.hfAmbient_compact {L : Language} (C : L.FinitaryCoding) (T : L.Theoryω) (hT : (hfAmbient C).ACEnumerable T) (hfin : (hfAmbient C).AFinitelySatisfiable T) : T.IsSatisfiable

The assembled HF compactness theorem, on the honest route end to end: both premises come from hfAmbient's own coding data, and the proof goes straight to finitaryFragment_compact — i.e. to Mathlib's first-order compactness.

Containment is discharged internally by hfAmbient_subset_finitary; the caller supplies only Σ-definability and the Barwise premise.

theorem FirstOrder.Language.hfAmbient_compactFor {L : Language} (C : L.FinitaryCoding) (T : L.Theoryω) : (hfAmbient C).CompactFor L.finitaryFragment T

HF inhabits the compactness interface.