すべての論理式の符号からなる集合

The equation is discharged with the index, the numeral and the environment all still variables; keeping them as variables is what avoids the extra conversion-checking overhead that later instantiation would otherwise incur.

Stating it takes 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. The whole formula has two existentials, one for the arity and one for the payload, the pair reader between them, and the membership on the arity.

Reading it in the other direction is where the choice takes effect. ω-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. Neither direction needs induction; the numeral chapter already did that work.

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.

Then the superset. smallDom asks for a small family of elements of L and returns a stage containing all of it; the family is indexed by the pairs of an arity and a formula at it. The type is 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.

The set is sealed where it is built. Unsealed, every later type mentioning it 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.

Introduction is the half that adds nothing beyond what is given. 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.

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 established.

The 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.