The theory layer (issue #19A)

The middle layer of the presentation tower:

FamilyPresentation        Element, IsFamilyCode, Index, DecodesFamily      -- syntax
        ↑
TheoryPresentation        + Mem, IsSentenceCode, decodeSentence
                          + derived IsTheoryCode / decodeTheory / AFinite  -- theories
        ↑
AmbientPresentation       + IsDefinitionCode, enumerates
                          + derived Sigma1                                 -- definability

The theory API stops here. AFinite and AFinitelySatisfiable take a TheoryPresentation, so at the type level they cannot mention definition codes, Sigma1, KP, or any numbering — those are defined in files that import this one. scripts/check_theory_cone.lean pins it.

That matters because the natural shortcut — define the production AFinite as AmbientPresentation.AFinite — would have made the whole theory interface depend on the Σ layer even though not one theory-side proof uses it.

What is derived rather than stored

IsTheoryCode and decodeTheory are not fields. Given ambient membership, a theory code is just an element all of whose members are sentence codes, and the theory it names is the decoded image of those members. Deriving them is what keeps Mem honest: a vacuous membership relation would collapse the theory layer, which a stored decodeTheory field would hide.

Functionality comes free: a theory code names an image, not a relation, so AFinite.unique is h ▸ h' and no extensionality law is needed even though sentence decoding is non-injective.

Totality is deliberately omitted. A presentation is not obliged to name every theory, and an honest HF must not: AFinite is existential over codes, never a bijection with theories.

Main definitions

• TheoryPresentation: the family view plus membership and sentence decoding.
• TheoryPresentation.decodeTheory, AFinite: the theory layer, derived from membership.
• TheoryPresentation.AFinitelySatisfiable: the Barwise premise.
• TheoryPresentation.AdequateFor: the decoded sentence range is exactly the intended fragment.

Main results

• TheoryPresentation.AFinite.subset_of_adequate: containment in the fragment is derived from adequacy, not assumed.

structure FirstOrder.Language.TheoryPresentation (L : Language) extends L.FamilyPresentation : Type (max (max (max u (uIndex + 1)) v) (w + 1))

The theory view of a presentation. The family view, plus ambient membership and sentence decoding — and nothing about definability.

decodeSentence is a function, so sentence decoding is functional by construction; it is not injective, since a sentence may have many codes.

• Element : Type w
• IsFamilyCode : self.Element → Prop
• Index : { e : self.Element // self.IsFamilyCode e } → Type uIndex
• indexEncodable (c : { e : self.Element // self.IsFamilyCode e }) : Encodable (self.Index c)
• DecodesFamily (n : ℕ) (c : { e : self.Element // self.IsFamilyCode e }) : (self.Index c → L.BoundedFormulaω Empty n) → Prop
• decodes_unique {n : ℕ} {c : { e : self.Element // self.IsFamilyCode e }} {f g : self.Index c → L.BoundedFormulaω Empty n} : self.DecodesFamily n c f → self.DecodesFamily n c g → f = g
• Mem : self.Element → self.Element → Prop

  Ambient membership. Without it the theory layer cannot be derived and closure obligations are vacuous.

• IsSentenceCode : self.Element → Prop

  Codes naming a single sentence.

• decodeSentence : { e : self.Element // self.IsSentenceCode e } → L.Sentenceω

  Stored sentence decoding on the sentence-code subdomain.

@[reducible, inline]

abbrev FirstOrder.Language.TheoryPresentation.SentenceCode {L : Language} (A : L.TheoryPresentation) : Type w

The sentence-code subdomain.

Equations

• A.SentenceCode = { e : A.Element // A.IsSentenceCode e }

def FirstOrder.Language.TheoryPresentation.sentenceRange {L : Language} (A : L.TheoryPresentation) : Set L.Sentenceω

The sentences the codes actually name.

Equations

• A.sentenceRange = Set.range A.decodeSentence

def FirstOrder.Language.TheoryPresentation.IsTheoryCode {L : Language} (A : L.TheoryPresentation) (e : A.Element) : Prop

Theory codes are derived, not stored: an element all of whose members are sentence codes.

Equations

• A.IsTheoryCode e = ∀ (x : A.Element), A.Mem x e → A.IsSentenceCode x

@[reducible, inline]

abbrev FirstOrder.Language.TheoryPresentation.TheoryCode {L : Language} (A : L.TheoryPresentation) : Type w

The theory-code subdomain.

Equations

• A.TheoryCode = { e : A.Element // A.IsTheoryCode e }

def FirstOrder.Language.TheoryPresentation.members {L : Language} (A : L.TheoryPresentation) (a : A.TheoryCode) : Set A.SentenceCode

The sentence codes belonging to a theory code. Well defined precisely because IsTheoryCode says every member is a sentence code.

Equations

• A.members a = {s : A.SentenceCode | A.Mem ↑s ↑a}

def FirstOrder.Language.TheoryPresentation.decodeTheory {L : Language} (A : L.TheoryPresentation) (a : A.TheoryCode) : L.Theoryω

The theory a code names: the decoded image of its members.

Equations

• A.decodeTheory a = A.decodeSentence '' A.members a

def FirstOrder.Language.TheoryPresentation.AFinite {L : Language} (A : L.TheoryPresentation) (T : L.Theoryω) : Prop

A-finiteness: the theory is named by a theory code — Barwise's "T₀ ∈ A".

Not external finiteness. It collapses to ordinary finiteness only at HF, and there only on the finitary fragment; see hfAmbient_aFinite_iff.

Equations

• A.AFinite T = ∃ (a : A.TheoryCode), A.decodeTheory a = T

def FirstOrder.Language.TheoryPresentation.AFinitelySatisfiable {L : Language} (A : L.TheoryPresentation) (T : L.Theoryω) : Prop

The Barwise premise: every A-finite subtheory is satisfiable.

Deliberately not Theoryω.IsFinitelySatisfiable, which quantifies over ordinarily finite subtheories. The two differ for every A beyond HF — A-finite means ∈ A, so for A = L(ω₁^CK) this quantifies over infinite hyperarithmetical subtheories as well.

Equations

• A.AFinitelySatisfiable T = ∀ T₀ ⊆ T, A.AFinite T₀ → T₀.IsSatisfiable

def FirstOrder.Language.TheoryPresentation.AdequateFor {L : Language} (A : L.TheoryPresentation) (F : Set L.Sentenceω) : Prop

Adequacy: the decoded sentence range is exactly the intended fragment.

Equations

• A.AdequateFor F = (A.sentenceRange = F)

@[simp]

theorem FirstOrder.Language.TheoryPresentation.mem_decodeTheory {L : Language} {A : L.TheoryPresentation} {a : A.TheoryCode} {φ : L.Sentenceω} : φ ∈ A.decodeTheory a ↔ ∃ (s : A.SentenceCode), A.Mem ↑s ↑a ∧ A.decodeSentence s = φ

theorem FirstOrder.Language.TheoryPresentation.AFinite.unique {L : Language} {A : L.TheoryPresentation} {a : A.TheoryCode} {T T' : L.Theoryω} (h : A.decodeTheory a = T) (h' : A.decodeTheory a = T') : T = T'

Functionality is free — a theory code names an image, not a relation, so this needs no extensionality law even though sentence decoding is non-injective.

theorem FirstOrder.Language.TheoryPresentation.decodeTheory_subset {L : Language} {A : L.TheoryPresentation} (a : A.TheoryCode) : A.decodeTheory a ⊆ A.sentenceRange

Codes cannot name sentences outside the decoded range.

theorem FirstOrder.Language.TheoryPresentation.AFinite.subset_of_adequate {L : Language} {A : L.TheoryPresentation} {F : Set L.Sentenceω} (hade : A.AdequateFor F) {T : L.Theoryω} (hT : A.AFinite T) : T ⊆ F

Containment, derived. decodeTheory_subset alone gives only a range bound; it becomes containment in the fragment exactly when adequacy identifies that range.