The ambient presentation: the definability layer (issue #19A)

The top of the presentation tower. One ambient Element type carries all codes; the four kinds — family, theory, sentence, Σ-definition — are subdomains of it and may overlap. In the HF instance every code is a natural number, so they overlap totally.

FamilyPresentation     Element, IsFamilyCode, Index, DecodesFamily      -- Admissible/Family.lean
        ↑
TheoryPresentation     + Mem, IsSentenceCode, decodeSentence            -- Admissible/Theory.lean
                       + derived IsTheoryCode / decodeTheory / AFinite
        ↑
AmbientPresentation    + IsDefinitionCode, enumerates                   -- this file
                       + derived Sigma1

Each layer is a separate file and each is imported by the next, so the syntax layer cannot reach the theory layer and the theory layer cannot reach definability — not by convention, by types and imports. scripts/check_family_cone.lean and scripts/check_theory_cone.lean pin both.

Why one carrier

Separate code sorts and a shared ambient type are inter-translatable (subtypes one way, Sum the other), so this is not a question of expressiveness. Two things decide it.

KP closure discriminates. Pairing and union are operations on elements; they do not respect the kind subdomains — the pair of a sentence code and a definition code is an element and typically has no kind at all. One carrier states such laws directly; separate sorts must route every closure law through Sum.

The kinds are roles, not sorts. The same codes — the elements of A — serve the family, theory, sentence and Σ-definition roles; only the thing named differs.

Sigma1 is derived

Because a Σ-definition code carries a set of sentence codes and the theory it defines is their decoded image, functionality holds by construction — Sigma1.unique is h ▸ h'. There is no extensionality law to discharge even though a sentence may have many codes.

Main definitions

• AmbientPresentation: the theory view plus the Σ-definition kind.
• AmbientPresentation.Sigma1: the definability layer.
• AmbientPresentation.WithKP: pairing and union, with specification laws.

Main results

• AmbientPresentation.subset_of_adequate: fragment containment for Σ-definable theories, derived from adequacy rather than assumed.

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

The ambient presentation. The theory view plus the Σ-definition kind.

enumerates returns a set of sentence codes, never a set of sentences — that is what makes Sigma1 functional for free.

• 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
• IsSentenceCode : self.Element → Prop
• decodeSentence : { e : self.Element // self.IsSentenceCode e } → L.Sentenceω
• IsDefinitionCode : self.Element → Prop

  Codes naming a Σ-definition, i.e. an intension. Contrast a theory code, which names a set of sentences extensionally.

• enumerates : { e : self.Element // self.IsDefinitionCode e } → Set { e : self.Element // self.IsSentenceCode e }

  Which sentence codes a Σ-definition code enumerates. Sets of codes, never of sentences.

@[reducible, inline]

abbrev FirstOrder.Language.AmbientPresentation.DefinitionCode {L : Language} (A : L.AmbientPresentation) : Type w

The Σ-definition-code subdomain.

Equations

• A.DefinitionCode = { e : A.Element // A.IsDefinitionCode e }

def FirstOrder.Language.AmbientPresentation.theoryOf {L : Language} (A : L.AmbientPresentation) (d : A.DefinitionCode) : L.Theoryω

The theory a Σ-definition code defines: the decoded image of the sentence codes it enumerates.

Equations

• A.theoryOf d = A.decodeSentence '' A.enumerates d

def FirstOrder.Language.AmbientPresentation.Sigma1 {L : Language} (A : L.AmbientPresentation) (T : L.Theoryω) : Prop

A-c.e., from the presentation's own coding data rather than an opaque predicate.

Equations

• A.Sigma1 T = ∃ (d : A.DefinitionCode), A.theoryOf d = T

@[simp]

theorem FirstOrder.Language.AmbientPresentation.mem_theoryOf {L : Language} {A : L.AmbientPresentation} {d : A.DefinitionCode} {φ : L.Sentenceω} : φ ∈ A.theoryOf d ↔ ∃ s ∈ A.enumerates d, A.decodeSentence s = φ

theorem FirstOrder.Language.AmbientPresentation.Sigma1.unique {L : Language} {A : L.AmbientPresentation} {d : A.DefinitionCode} {T T' : L.Theoryω} (h : A.theoryOf d = T) (h' : A.theoryOf d = T') : T = T'

Functionality is free — the theory is an image, not a relation.

theorem FirstOrder.Language.AmbientPresentation.theoryOf_subset {L : Language} {A : L.AmbientPresentation} (d : A.DefinitionCode) : A.theoryOf d ⊆ A.sentenceRange

Σ-definable theories cannot escape the decoded range.

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

Containment for the Σ-layer, derived. This is what lets a presentation-relative compactness wrapper discharge the T ⊆ P hypothesis internally, using the presentation's own Sigma1 rather than a free parameter.

The compactness interface

Both come from the presentation's own definition codes, rather than from a bare external Sigma1 predicate carrying no representation data.

def FirstOrder.Language.AmbientPresentation.ACEnumerable {L : Language} (A : L.AmbientPresentation) (T : L.Theoryω) : Prop

A-c.e.: the theory is Σ₁-on-A.

Not an arbitrary Prop on a set: unfolding it produces a definition code, which is what makes subset_of_adequate available at all.

Equations

• A.ACEnumerable T = A.Sigma1 T

def FirstOrder.Language.AmbientPresentation.CompactFor {L : Language} (A : L.AmbientPresentation) (P T : L.Theoryω) : Prop

The shape of a Barwise-style compactness statement over a permitted sentence set P.

T ⊆ P stays a genuine hypothesis. It is not removed: subset_of_adequate yields it only once an adequacy equation identifies the decoded range with P, and a presentation need not be adequate for the P a caller has in mind. compactFor_of_adequate below is the wrapper that discharges it where adequacy is available.

Both premises enter as hypotheses, so no instance can claim this shape while secretly projecting a compactness field — there is none to read.

Equations

• A.CompactFor P T = (T ⊆ P → A.ACEnumerable T → A.AFinitelySatisfiable T → T.IsSatisfiable)

theorem FirstOrder.Language.AmbientPresentation.acEnumerable_def {L : Language} {A : L.AmbientPresentation} {T : L.Theoryω} : A.ACEnumerable T ↔ A.Sigma1 T

theorem FirstOrder.Language.AmbientPresentation.compactFor_of_adequate {L : Language} {A : L.AmbientPresentation} {P T : L.Theoryω} (hcompact : A.CompactFor P T) (hade : A.AdequateFor P) (hce : A.ACEnumerable T) (hfin : A.AFinitelySatisfiable T) : T.IsSatisfiable

The assembly theorem. A consumer holding compactness and adequacy never supplies containment: it follows from Σ-definability, because a definition code enumerates sentence codes and those decode into the fragment and nowhere else.

This is the payoff of Sigma1 carrying coding data rather than being a bare predicate: a bare Prop on a set carries nothing from which containment could be derived.

KP closure, with specification laws

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

Pairing and union, stated meaningfully.

The earlier sketch carried only totality — pair_total : ∀ a b, ∃ c, Pair a b c — which is satisfied by Pair := fun _ _ _ => True on any inhabited carrier. Totality is not pairing. Here each operation is pinned by a specification law against Mem, so the fields cannot be discharged trivially.

Only pairing and union appear. The full KP schema is deliberately not attempted: the #19A source audit must first identify which closure and absoluteness laws later proofs actually consume.

• 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
• IsSentenceCode : self.Element → Prop
• decodeSentence : { e : self.Element // self.IsSentenceCode e } → L.Sentenceω
• IsDefinitionCode : self.Element → Prop
• enumerates : { e : self.Element // self.IsDefinitionCode e } → Set { e : self.Element // self.IsSentenceCode e }
• pair : self.Element → self.Element → self.Element

  The unordered pair.

• mem_pair (a b x : self.Element) : self.Mem x (self.pair a b) ↔ x = a ∨ x = b

  Its specification — the law the bare totality field lacked.

• union : self.Element → self.Element

  The union.

• mem_union (a x : self.Element) : self.Mem x (self.union a) ↔ ∃ (y : self.Element), self.Mem y a ∧ self.Mem x y

  Its specification.