BedrockThe codes, as one set
Every chapter so far has been careful to say that the set of all codes is not an element of L, and that nothing needed it. Two things need it now, and they want different sets. The definable powerset takes syntax as its index type, Def A = sett (Formula ⟪A⟫ 1) defSet, so internalizing definability at a stage means naming the arity-one formulas over that stage from inside the model, and a formula can only name a set. The satisfaction recursion wants an index set closed under subcodes, and a quantifier's subformula lives one arity up, so it wants the keys at every arity instead.
Neither set is built by collecting the codes. Each is cut out of a superset:
smallDom contains any small family of elements of L in a single stage, the keys are such a family, and separation inside L holds for formulas of any complexity. So the chapter is two object-language predicates that differ in one conjunct, and the two directions of adequacy for each.
The predicate has two conjuncts and they are not of equal weight. The second one, "there merely is a carrier equal to A and a set C with x a member of it, C closed and C shaped at that carrier", is unbounded existentials and costs nothing here: satisfaction is read at the class model, where an existential ranges over L and no stage has to reflect anything.
The first conjunct is the load-bearing one, and it is the finding. recover does not take a member of a closed and shaped set; it takes a member handed over as a key at a stated arity, and nothing in closedAt or
shapedAt constrains the arity slot. Shapedness binds the arity existentially and puts no condition on it, so a set holding a pair whose first component is not a numeral at all satisfies both halves, and the decode has nothing to say about that pair. That debt was recorded where it was incurred, and this is where it is paid: the predicate says, from outside, that x is a pair whose first component is a numeral. Which numeral is the only difference between the two predicates. The arity-one set names it, the all-arity set binds it and requires only that it lie in ωʟ, and everything else in the chapter is shared verbatim.
The carrier is a slot, and one binder above the slot is what turns it into a constant. Shapedness takes its carrier as a slot, so something has to occupy that slot; hasWitnessAt leaves the slot to its caller, and hasWitness occupies it with a bound variable pinned by var zero ≐ con A.
Splitting it that way is forced, and the reason is the consumer rather than this chapter. The internal hierarchy binds its stage, so the definable powerset has to be described at a carrier that is a bound variable, and a set enters a formula only by being named as a constant. A predicate that names its carrier therefore cannot be spoken under that binder at all, which is why the carrier had to stop being a constant here. Pinning is what an instance that does hold the carrier as a set of its own does afterwards, and the pinned form is one existential longer than the general one: that binder existed only to name the constant.
Which half is hard, then, is settled. Introduction is three lemmas already proved, applied to the subformula closure. Elimination is where the arity conjunct is spent, and without it there is no elimination at all.
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Truth open import Base.Classical using ( LEM ) module L.Coding.CodeSet {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; ∃̇_ ) open import FOL.Manipulation.Relabelling using ( mapFo ) import FOL.Absoluteness import FOL.ZFModel open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Coding {ℓ} using ( pr; module VCode ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans ) open import L.Recursion {ℓ} lem using ( smallDom ) open import L.Axioms.Full {ℓ} lem using ( hasSeparationL ) open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst ) open import L.Axioms.Infinity {ℓ} lem using ( ωʟ; ω-specL ) open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; tagAtL; tagAtL-adequate; closedAt ) open import L.Coding.InL {ℓ} using ( key; keyL; codeL; key∈closure ) open import L.Coding.Closed {ℓ} using ( clo; closureClosed ) open import L.Coding.Shape {ℓ} using ( shapedAt; closureShaped ) open import L.Coding.Recover {ℓ} using ( keyOf-fst; module Decode ) open import Cubical.Functions.Logic using ( ⇔toPath ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ ) open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪; ∈∈ₛ; ∈ₛ⟪_⟫↪_; ∈-asFiber ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet using ( #_ ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁; squash₁ ) open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ)) open hPropStructure 𝒮ʟ module ModelL = FOL.ZFModel 𝒮ʟ open ModelL using ( SetOf ) module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
Is a key at a stated arity
One reader, and it is the only new piece of object language the chapter needs. A key at arity k is a pair whose first component is the numeral k, and the tag reader already says exactly that of a named second component. What is wanted here is the second component left unnamed, so the reader is the tag reader under one existential, and its two directions are the existential's two directions with the tag reader's adequacy equation discharged inside.
The equation is discharged with the index, the numeral and the environment all still variables, because that is the only way it is cheap. Both call sites below are at a fixed index and a fixed numeral, and neither pays for the unfolding.
keyArityAtL : ∀ {n} → Fin n → ℕ → Formula S n keyArityAtL c k = ∃̇ (tagAtL (suc c) k zero) keyArityAtL-out : ∀ {n} (c : Fin n) (k : ℕ) (γ : S ^ n) → ⟨ γ ⊨ keyArityAtL c k ⟩ → ∥ (Σ[ z ∈ S ] (fst (lookup c γ) ≡ pr (# k) (fst z))) ∥₁ keyArityAtL-out c k γ = PT.map (λ { (z , hz) → z , subst ⟨_⟩ (tagAtL-adequate (suc c) k zero (z ∷ γ)) hz }) keyArityAtL-in : ∀ {n} (c : Fin n) (k : ℕ) (γ : S ^ n) (z : S) → fst (lookup c γ) ≡ pr (# k) (fst z) → ⟨ γ ⊨ keyArityAtL c k ⟩ keyArityAtL-in c k γ z e = ∣ z , subst ⟨_⟩ (sym (tagAtL-adequate (suc c) k zero (z ∷ γ))) e ∣₁
Is a key at some arity
The reader above names its arity as a metalevel numeral, which is what pins the arity to one; a set that has to hold subcodes cannot do that, because a quantifier's subformula lives one arity up. So the arity has to become a bound set, and something has to say of that set what # k said for free: that it is a numeral.
Saying it costs one constant. ωʟ is an element of L whose members are exactly the numerals, so "the arity component lies in ωʟ" is the condition, written with the same unbounded membership the second conjunct already uses. Two existentials, one for the arity and one for the payload, the pair reader between them, and the membership on the arity.
Reading it back is where the choice pays. ω-specL is an equation between propositions, not an implication, so a member of ωʟ is a truncated natural number, and one composition with the chain's projection equation turns it into the metalevel # m that recover takes as its arity argument. There is no induction in either direction; the numeral chapter did it.
arityNumAtL : ∀ {n} → Fin n → Formula S n arityNumAtL c = ∃̇ (∃̇ (prAtL (suc (suc c)) (suc zero) zero ∧̇ (var (suc zero) ∈̇ con ωʟ))) arityNumAtL-out : ∀ {n} (c : Fin n) (γ : S ^ n) → ⟨ γ ⊨ arityNumAtL c ⟩ → ∥ (Σ[ m ∈ ℕ ] Σ[ z ∈ S ] (fst (lookup c γ) ≡ pr (# m) (fst z))) ∥₁ arityNumAtL-out c γ = PT.rec squash₁ (λ { (ar , h) → PT.rec squash₁ (λ { (z , (hp , hω)) → PT.map (λ { (m , qm) → lower m , z , ( subst ⟨_⟩ (prAtL-adequate (suc (suc c)) (suc zero) zero (z ∷ ar ∷ γ)) hp ∙ cong (λ w → pr w (fst z)) (qm ∙ numeralL-fst (lower m)) ) }) (subst ⟨_⟩ (ω-specL ar) hω) }) h }) arityNumAtL-in : ∀ {n} (c : Fin n) (γ : S ^ n) (m : ℕ) (z : S) → fst (lookup c γ) ≡ pr (# m) (fst z) → ⟨ γ ⊨ arityNumAtL c ⟩ arityNumAtL-in c γ m z e = ∣ numeralL m , ∣ z , ( subst ⟨_⟩ (sym (prAtL-adequate (suc (suc c)) (suc zero) zero (z ∷ numeralL m ∷ γ))) (e ∙ cong (λ w → pr w (fst z)) (sym (numeralL-fst m))) , subst ⟨_⟩ (sym (ω-specL (numeralL m))) ∣ lift m , refl ∣₁ ) ∣₁ ∣₁
The predicate
Two conjuncts, at one free variable. The first pins the arity from outside, which is the conjunct the previous chapter asked for by name. The second is a witness for the decode's two hypotheses: a set holding the argument, closed and shaped.
Nothing in the second conjunct is bounded, and nothing has to be. The witness is produced from a formula's own subformula closure in the introduction, and consumed as a set of L in the elimination, and the class model is where both readings happen.
The second conjunct is written twice: once at two slots, the carrier and the argument, and once with the carrier pinned to a constant. The general one is a single existential, for the set; the pinned one wraps it in the binder that names A, and that binder is the entire difference between them. Both predicates below take the pinned form verbatim, and so do both halves of both adequacy proofs; what separates the two predicates is the arity conjunct and nothing else.
hasWitnessAt : ∀ {n} → Fin n → Fin n → Formula S n hasWitnessAt A x = ∃̇ ((var (suc x) ∈̇ var zero) ∧̇ (closedAt zero ∧̇ shapedAt zero (suc A))) hasWitness : S → Formula S 1 hasWitness A = ∃̇ ((var zero ≐ con A) ∧̇ hasWitnessAt zero (suc zero)) isCode : S → Formula S 1 isCode A = keyArityAtL zero 1 ∧̇ hasWitness A isCodeAny : S → Formula S 1 isCodeAny A = arityNumAtL zero ∧̇ hasWitness A
The superset, and the set
The carrier is fixed, and the consumer will fix it at a stage. Its members are the alphabet, exactly as the coding chapters' two parameters expect: the embedding into the hierarchy, and the certificate that what it lands on is constructible. The second is transitivity of L applied once, and the membership it is applied to is named separately, because the shape predicate now asks for it in its own right.
Then the supersets, one for each set. smallDom asks for a small family of elements of L and returns a stage containing all of it; the arity-one family is indexed by the arity-one formulas over the alphabet, and the all-arity family by the pairs of an arity and a formula at it. Both are types of the right size because syntax is an inductive type at the alphabet's own level, and the arity is a natural number, which costs no level at all. What comes back contains every key and much else, and separation removes the else.
Both sets are sealed where they are built. Unsealed, every later type mentioning one would carry the separation instrument's unfolding into conversion, and the facts exported here are all any consumer needs. Only the ones that read a separation are inside a seal; the directions back and the equations they compose into are outside, since none of them needs to know what the set was cut out of.
module _ (A : S) where private ι : ⟪ fst A ⟫ → V ℓ ι = ⟪ fst A ⟫↪ ι∈ : (m : ⟪ fst A ⟫) → ⟨ ι m ∈ fst A ⟩ ι∈ m = ∈∈ₛ {a = ι m} {b = fst A} .snd (∈ₛ⟪ fst A ⟫↪ m) ιL : (m : ⟪ fst A ⟫) → ⟨ isL (ι m) ⟩ ιL m = isL-trans {x = fst A} {y = ι m} (ι∈ m) (A .snd) codeS : ∀ {n} → Formula ⟪ fst A ⟫ n → S codeS φ = VCode.⌜ mapFo ι φ ⌝ , codeL ι ιL φ keyS : ∀ {n} → Formula ⟪ fst A ⟫ n → S keyS φ = key ι ιL φ , keyL ι ιL φ private small : Σ[ d ∈ S ] ((φ : Formula ⟪ fst A ⟫ 1) → ⟨ keyS φ ∈ˢ d ⟩) small = smallDom (Formula ⟪ fst A ⟫ 1) keyS sep : isContr (SetOf (λ x → (x ∈ˢ small .fst) ⊓ ((x ∷ []) ⊨ isCode A))) sep = hasSeparationL (small .fst) (isCode A) smallAny : Σ[ d ∈ S ] ((p : Σ[ n ∈ ℕ ] Formula ⟪ fst A ⟫ n) → ⟨ keyS (snd p) ∈ˢ d ⟩) smallAny = smallDom (Σ[ n ∈ ℕ ] Formula ⟪ fst A ⟫ n) (λ p → keyS (snd p)) sepAny : isContr (SetOf (λ x → (x ∈ˢ smallAny .fst) ⊓ ((x ∷ []) ⊨ isCodeAny A))) sepAny = hasSeparationL (smallAny .fst) (isCodeAny A)
The witness, in and out
Both halves of the second conjunct are proved here, once, at a variable arity, a variable carrier slot and a variable environment, and everything below applies them. The arity may be variable because the conjunct never mentions it: the introduction produces a closed, shaped set for a formula of any arity, and the elimination consumes one and calls the decode, which took the arity as an argument from the start. The carrier and the environment may be variable because every lemma the two halves are built from already takes them so.
Introduction is the half with nothing in it. The witness is the subformula closure, whose three obligations are key∈closure, closureClosed and closureShaped, one chapter each and all already discharged. The last of them asks for one thing more, that every constant is a member of the carrier, and at this alphabet that is the fact the alphabet was defined by, carried across the slot's equation.
Elimination is the other half, and it starts from the member already in key form at a stated arity, which is what recover demands and what nothing in the second conjunct would supply. The carrier slot's equation turns a membership in whatever that slot holds into a membership in A, which is what makes the decode's hypothesis dischargeable: A's members are exactly the image of ⟪ A ⟫, by the presentation of a set by its own members. Read the existential and a closed, shaped set arrives with it. Then the decode runs, and its answer is a formula over the carrier, at the arity it was handed.
The pinned pair is these two at the environment the naming binder makes, and that is the whole of what pinning costs: introduction supplies A for the binder and refl for its equation, elimination reads the binder off and hands what it holds to the general form. Reading it off is where the payload has to be named. Left to inference, the truncation's payload at a pinned carrier is a metavariable standing for the satisfaction of a formula the elaborator has not committed to, and the same two lines that check in two seconds with the type written out ran past 140 seconds without it and were killed there. This is the law the recursion's totality hypothesis recorded, met again in a different place: it is not about the graph, it is about PT.rec at a concrete environment.
witnessAt-in : ∀ {n k} (b c : Fin n) (γ : S ^ n) (φ : Formula ⟪ fst A ⟫ k) → fst (lookup b γ) ≡ fst A → fst (lookup c γ) ≡ fst (keyS φ) → ⟨ γ ⊨ hasWitnessAt b c ⟩ witnessAt-in b c γ φ qb qc = ∣ clo ι ιL φ , ( subst (λ w → ⟨ w ∈ fst (clo ι ιL φ) ⟩) (sym qc) (key∈closure ι ιL φ) , ( closureClosed ι ιL φ γ , closureShaped ι ιL φ b γ (λ m → subst (λ w → ⟨ ι m ∈ w ⟩) (sym qb) (ι∈ m)) ) ) ∣₁ witnessAt-out : ∀ {n} (b c : Fin n) (γ : S ^ n) → fst (lookup b γ) ≡ fst A → ⟨ γ ⊨ hasWitnessAt b c ⟩ → (k : ℕ) (z : S) → fst (lookup c γ) ≡ pr (# k) (fst z) → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ k ] (fst (lookup c γ) ≡ fst (keyS ψ))) ∥₁ witnessAt-out b c γ qb hw k z qz = PT.rec squash₁ viaSlot hw where Target : Type (ℓ-suc ℓ) Target = ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ k ] (fst (lookup c γ) ≡ fst (keyS ψ))) ∥₁ onto : (y : V ℓ) → ⟨ y ∈ fst (lookup b γ) ⟩ → ∥ Σ[ m ∈ ⟪ fst A ⟫ ] (ι m ≡ y) ∥₁ onto y y∈ = ∣ ∈-asFiber {a = y} {b = fst A} (subst (λ w → ⟨ y ∈ w ⟩) qb y∈) ∣₁ viaSlot : Σ[ C ∈ S ] ⟨ (C ∷ γ) ⊨ ((var (suc c) ∈̇ var zero) ∧̇ (closedAt zero ∧̇ shapedAt zero (suc b))) ⟩ → Target viaSlot (C , (x∈C , (hcl , hsh))) = PT.map (λ { (ψ , qψ) → ψ , (qz ∙ cong (pr (# k)) (sym qψ)) }) (Decode.recover ι zero (suc b) (C ∷ γ) onto hcl hsh k z (subst (λ w → ⟨ w ∈ fst C ⟩) (qz ∙ sym (keyOf-fst k z)) x∈C)) private witness-in : ∀ {n} (φ : Formula ⟪ fst A ⟫ n) → ⟨ (keyS φ ∷ []) ⊨ hasWitness A ⟩ witness-in φ = ∣ A , ( refl , witnessAt-in zero (suc zero) (A ∷ keyS φ ∷ []) φ refl refl ) ∣₁ witness-out : (x : S) → ⟨ (x ∷ []) ⊨ hasWitness A ⟩ → (k : ℕ) (z : S) → fst x ≡ pr (# k) (fst z) → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ k ] (fst x ≡ fst (keyS ψ))) ∥₁ witness-out x hw k z qz = PT.rec squash₁ viaCarrier hw where viaCarrier : Σ[ B ∈ S ] ⟨ (B ∷ x ∷ []) ⊨ ((var zero ≐ con A) ∧̇ hasWitnessAt zero (suc zero)) ⟩ → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ k ] (fst x ≡ fst (keyS ψ))) ∥₁ viaCarrier (B , (qB , hB)) = witnessAt-out zero (suc zero) (B ∷ x ∷ []) qB hB k z qz
Both directions, and they meet
The statement both directions are about is written first, and it is one class: the keys, at arity one, of the formulas over the carrier. Introduction says every such key is a member and elimination says every member is such a key, so the two are no longer two bounds on the set but one characterization of it.
What is left of each direction, once the witness is factored out, is the arity conjunct. Introduction adds two things to witness-in: membership in the superset, by the family the key indexes, and the arity conjunct, whose witness is the code and whose equation is refl. Elimination reads the arity conjunct first, because without it the member does not arrive in key form at all, and hands what it reads to witness-out.
IsKeyOver : S → Ω IsKeyOver x = ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ 1 ] (fst x ≡ fst (keyS ψ))) ∥₁ , squash₁ opaque Codes : S Codes = sep .fst .fst key∈Codes : (φ : Formula ⟪ fst A ⟫ 1) → ⟨ keyS φ ∈ˢ Codes ⟩ key∈Codes φ = subst ⟨_⟩ (sym (sep .fst .snd (keyS φ))) ( small .snd φ , ( keyArityAtL-in zero 1 (keyS φ ∷ []) (codeS φ) refl , witness-in φ ) ) Codes-out : (x : S) → ⟨ x ∈ˢ Codes ⟩ → ⟨ IsKeyOver x ⟩ Codes-out x x∈ = PT.rec squash₁ (λ { (z , qz) → witness-out x (sat .snd) 1 z qz }) (keyArityAtL-out zero 1 (x ∷ []) (sat .fst)) where sat : ⟨ (x ∷ []) ⊨ isCode A ⟩ sat = subst ⟨_⟩ (sep .fst .snd x) x∈ .snd Codes-in : (x : S) → ⟨ IsKeyOver x ⟩ → ⟨ x ∈ˢ Codes ⟩ Codes-in x = PT.rec (snd (x ∈ˢ Codes)) (λ { (ψ , q) → subst (λ w → ⟨ w ∈ fst Codes ⟩) (sym q) (key∈Codes ψ) }) Codes-spec : (x : S) → (x ∈ˢ Codes) ≡ IsKeyOver x Codes-spec x = ⇔toPath (Codes-out x) (Codes-in x)
The round trip
The two directions are now stated over the same alphabet, and they compose into an equation between propositions: a member of Codes is exactly a key of a formula over the carrier. The direction back is one substitution, because membership depends on the underlying set alone and a key is one; nothing has to be reproved, since key∈Codes already put every such key in.
The conjunct that closed it was isTmAt's, and it is worth saying plainly what was wrong before. A variable's index was bounded, by the arity numeral; a constant's payload was bounded by nothing, so the clause said only "there is something, and the payload is its tag", and the something was an arbitrary element of L. A formula recovered from a member could therefore name constants outside the carrier, and no reading of the old predicate ruled it out. The set was caught between two statements: every formula over the carrier had its key in it, and every member came back as a formula over the model. Those are not the same class. They are now, and the bound on the constants is the whole of the difference.
The same set at every arity
The second set differs from the first in one conjunct and one index type, and its adequacy is the same two lines with the arity carried along. What comes out is the class of keys of formulas over the carrier at any arity, which is the class a recursion over subcodes has to be indexed by, because a quantifier's subformula lives one arity up and the arity-one class does not contain it.
The arity-one set is left exactly as it was, and that is a decision worth stating. It could be cut out of the all-arity set by the old arity conjunct, but the elimination would then have to turn "a key at some arity n, and the arity is one" back into a formula at arity one, which means inverting the numeral and transporting a formula along the resulting equation. That is more work than the separation it would replace, and the two sets share everything that was expensive already: one witness introduction, one witness elimination, one decode.
IsKeyOverAny : S → Ω IsKeyOverAny x = ∥ (Σ[ n ∈ ℕ ] Σ[ ψ ∈ Formula ⟪ fst A ⟫ n ] (fst x ≡ fst (keyS ψ))) ∥₁ , squash₁ opaque AllCodes : S AllCodes = sepAny .fst .fst key∈AllCodes : ∀ {n} (φ : Formula ⟪ fst A ⟫ n) → ⟨ keyS φ ∈ˢ AllCodes ⟩ key∈AllCodes {n} φ = subst ⟨_⟩ (sym (sepAny .fst .snd (keyS φ))) ( smallAny .snd (n , φ) , ( arityNumAtL-in zero (keyS φ ∷ []) n (codeS φ) refl , witness-in φ ) ) AllCodes-out : (x : S) → ⟨ x ∈ˢ AllCodes ⟩ → ⟨ IsKeyOverAny x ⟩ AllCodes-out x x∈ = PT.rec squash₁ (λ { (k , z , qz) → PT.map (λ { (ψ , q) → k , ψ , q }) (witness-out x (sat .snd) k z qz) }) (arityNumAtL-out zero (x ∷ []) (sat .fst)) where sat : ⟨ (x ∷ []) ⊨ isCodeAny A ⟩ sat = subst ⟨_⟩ (sepAny .fst .snd x) x∈ .snd AllCodes-in : (x : S) → ⟨ IsKeyOverAny x ⟩ → ⟨ x ∈ˢ AllCodes ⟩ AllCodes-in x = PT.rec (snd (x ∈ˢ AllCodes)) (λ { (n , ψ , q) → subst (λ w → ⟨ w ∈ fst AllCodes ⟩) (sym q) (key∈AllCodes ψ) }) AllCodes-spec : (x : S) → (x ∈ˢ AllCodes) ≡ IsKeyOverAny x AllCodes-spec x = ⇔toPath (AllCodes-out x) (AllCodes-in x)
Recap
Two sets, and one predicate apart. Codes is an element of L whose members are exactly the arity-one keys of the formulas over the carrier, by
Codes-spec, which is the statement the definable powerset needs, since
Def A indexes by that class and no other. AllCodes is the same construction with the arity bound instead of named, and AllCodes-spec pins it to the keys at every arity.
The whole content is in two conjuncts, and both are of the same kind. Closedness and shapedness together recognize the shape of a code and say nothing about the arity a key carries or the alphabet its constants come from, so a decode written against them has to be handed both, and a set built from them has to state both.
smallDom and general-formula separation do the rest, and neither needed anything the earlier chapters had not already paid for.
The all-arity set exists for the class it characterizes, not for a theorem about it. A recursion over codes has to answer at a code's subcodes, a quantifier's subformula lives one arity up, and the arity-one class does not contain it, so the domain has to be the keys at every arity. What the arity conjunct changed, from a metalevel numeral to membership in ωʟ, is the whole of the difference between a set a recursion can be indexed by and a set it cannot.