定義可能な冪集合を表す論理式

This is the step the whole route exists for. Every chapter before it built a component at a carrier the caller holds: a set of L, named in a formula as a constant. The internal hierarchy cannot hold its stage that way. Its graph binds the stage, because a graph may not name the object it defines, and a set enters a formula only by being named. So the description of the definable powerset has to be speakable under that binder, with the carrier occupying a slot of the ambient environment and nothing else.

What the description says is what the operator is. u is the definable powerset of the carrier when its members are exactly the sets carved out of the carrier by a formula: there merely is a code c over the carrier and a value v, the value is what the satisfaction recursion records at that code, and u's member is the set of members of the carrier whose one-entry environment lies in v. Three conjuncts, and each is a chapter already delivered, read at a slot rather than at a constant.

One shape correction is forced and it is worth stating before the formula appears. The code and the value are bound by adjacent existentials, with no conjunct between them. Nested through an intervening conjunct the two hypotheses land at different environments, and the route would acquire a weakening lemma it otherwise never needs: the same formula, the same conjunct count, the same depth, and a lemma's worth of difference.

Definability at arity one asks whether a formula holds of a single member, and the satisfaction recursion answers at environments, so the two are joined by the environment that assigns that member to the only variable there is. An environment is its graph, and a graph of length one is a single pair: the numeral zero with the value.

That makes the reader one line. "The set at this slot has exactly the pairs (0, y) as members" is extAt applied to the tag reader, and the tag reader already delivers the equation between underlying sets, so nothing has to be proved about pairs here at all.

Its two directions are hand-written over the one-element index type, and that is a measurement rather than a taste. Reading a membership in a one-entry set back is a two-case split, one case impossible; through a library round trip between finite functions and vectors the same statement walled a chapter at over eight minutes, and the chapter that met it wrote its two clauses by hand instead. This one does the same.

The third conjunct, alone, at three slots: the member, the carrier and the value the satisfaction recursion recorded. It says that the member is the set of those members of the carrier whose one-entry environment lies in that value, which is the definable subset spelled out with the recursion in the place of satisfaction.

The condition is a conjunction rather than one clause because the carrier's bound is not implied by the rest. A member of the recursion's value is an environment, not a set of the carrier, so the second half alone would say nothing about where the member came from; the definable subset is cut out of the carrier and the formula has to say so.

Its two directions are extAt's own two, and the existential inside the condition is read by the previous section. Nothing here inspects the value, which is why this section knows nothing about codes.

Two conjuncts, both already proved, and this is only where they meet: the argument is a key at arity one, and it has a closed, shaped witness at the carrier the slot holds. The first is what tells the decode which arity to answer at; the second is what the decode runs on. Neither names a set, so the pair can be stated under any binder.

The pinned predicate of the code-set chapter is this same pair with one binder on top, and that binder is the only thing separating a predicate a stage can hold from a predicate a bound variable can carry.

The satisfaction recursion's graph was generalized to take its carrier as a slot, and its two halves are the existence and uniqueness the recursion was built from, restated at that slot and at a variable environment. Nothing is proved here that was not proved then: existence hands over the subformula slot, the table over it, and the ten clauses, all three of which take the ambient environment as an argument already; uniqueness reads the graph's own bound index set and table back and applies the pinning theorem at the carrier the graph bound.

Both are stated with the code and the value reached by equations rather than named, which is the law the value theorems were written under: naming a key puts its construction inside a satisfaction, and the same statement then costs minutes instead of seconds.

The three conjuncts, under two adjacent existentials, under one extension: u is the set of exactly those x for which there merely are a code c over the carrier and a value v such that the recursion records v at c and x is what v defines. That is the definable powerset, said in the object language, with the carrier at a slot throughout.

The side condition is about what an object-language quantifier can reach. Every existential in the description ranges over L, so the set the description picks out can only contain constructible sets. If some definable subset of the carrier were not constructible, the description would still be satisfied, by the set of the constructible ones, and it would then hold of something that is not the definable powerset. DefOK is exactly the absence of that gap.

A carrier the caller holds needs no such condition stated, because a caller that holds the carrier holds the theorem about it too. A carrier at a slot is whatever the ambient environment puts there, and no theorem about it is available under the binder, so the fact has to travel as a hypothesis and be discharged where the slot is filled. It is a hypothesis of the elimination only: the introduction is given that u is the definable powerset, and u is an element of L, so its members are constructible already and the condition it would have needed is implied by its own hypothesis.

The two halves of the description at a single formula, which is what the adequacy is assembled from. Supplying the three conjuncts for a formula ψ is supplying its key for the code and the recursion's value for the value; reading them back is decoding the code to a formula, pinning the value to the recursion's own, and then reading the third conjunct as a set identity.

Everything here is stated at a variable carrier reached by an equation, and that is what keeps the stage out of the proof. The instantiation at a stage is an equation the caller supplies, and neither Lset nor an ordinal appears anywhere below.

Assembling and describing are the per-member halves, and the two readings are those under extAt's own two directions. The introduction says that the definable powerset satisfies the description: every member of it is a definable subset, and the three conjuncts are supplied for the formula that defines it. The elimination says that nothing else does, and it is the direction the side condition is for, since a set the description holds of has to be re-entered member by member, and each member either is an element of L or is absent altogether.

The instantiation is just one equation. A stage is an element of L, its definable subsets are constructible because a stage is constructible one stage later, and those two facts are what the successor identity delivers at every stage at once. So the side condition is discharged for good, and what is left is an equivalence of truth values: at a carrier holding a stage, the description holds of a set exactly when that set is the definable powerset of that stage. It holds of 𝒟ₒS and of nothing else.

Neither statement mentions the stage as anything but the value of a slot, which is what the internal hierarchy needs: the description will be spoken under a binder, and the equation the caller supplies is the only thing that connects it to a stage at all.

DefAt is the definable powerset described in the object language at a carrier that is a slot, and DefAt-in and DefAt-out are its two readings: the operator satisfies the description, and under DefOK nothing else does. DefAt-stage instantiates both readings at a stage, where the side condition is discharged once and for all and the description becomes an equation between truth values.

Three chapters meet here and not one of them is re-proved. The code predicate is read at a slot, the satisfaction graph is read at a slot, and the definable subset is read through the bridge that says the recursion's value is satisfaction over the carrier. What is new is only the joining: envOneAt, one line, because an environment of length one is a single pair, and DefinesAt, which is extAt over a two-part condition.

Two measurements are worth recording. The adjacency correction was adopted before the first line was written and it cost nothing, so no weakening lemma exists anywhere on this route. And the one difficulty met while writing was not in the mathematics at all: the code predicate's elimination at a pinned carrier, with the truncation's payload left to inference, ran past 140 seconds and was terminated there, while the same two lines with the payload type written out check in two seconds. Every PT.rec here names its payload, and that is why this chapter checks in half a minute rather than not at all.