任意の論理式に対する反映

The proof is structural induction, and it needs two things of the stage. At an unbounded quantifier it needs the previous chapter's closure, for the quantifier's own matrix. At a bounded quantifier it needs the bound to lie in the stage, so that anything the bound admits does too; that is the constants condition the separation chapter already knows how to meet.

No single-matrix limit can serve all the matrices at once, because closure is not inherited by larger stages: enlarging the stage admits more environments to answer for. So the ladder is built jointly. One rung's step merges, over the formula's structure, the single-matrix step of every matrix in it, together with the stage holding the constants. The limit then answers for every matrix, and the previous chapter's argument applies to each without being run again.

lint-agda: keep (⊤̇ names the defining formula behind LsetS)

The certificate is sealed, and only it: the stage as an element of the model is the pair of the stage with the certificate, and the first component has to keep reducing, since "lies in the bound" and "lies in the stage" are the same statement only because it does. The certificate is a different matter. It unfolds through definability into the smallness machinery, and it sits inside a constant, so every consumer that mentions the constant in a type would carry that unfolding along; a chapter that separates with a relativized formula takes minutes rather than seconds without this one line.

A universal quantifier contributes the step for the negated matrix, because the argument for it is by contradiction: to know that everything in the stage satisfies the matrix is to know that nothing in L refutes it, and the refutation is what has to be included in the stage.

These conditions only grow easier to satisfy as the rung grows, since each entry is a membership and membership is inherited through an ordinal. That is what lets the merges below raise the pieces to their join.

Each shape is written once, over an arbitrary payload with an arbitrary way of raising it, so the recursion itself is ten one-line clauses and the ordinal bookkeeping is not restated at each. The alternative, which is what one writes first, is three parallel recursions of ten clauses each computing the ordinal, its ordinality, and the rung's membership in it; they all traverse the same tree and project the same bounds.

Two readings come off the step for free, because they were built into it. The extra ordinal is in the first rung, hence under the limit. And at every rung, the whole tree of memberships holds against the next rung, which is the answering hypothesis in the form the induction wants.

Reading these conditions back off gives closure. At a rung, the tree gives that the matrix's step function lies inside the next rung, and the previous chapter gives that the matrix's answering stage is inside its step function; ordinal transitivity composes them into the answering hypothesis, and the ladder's closure follows.

Two auxiliary facts let the induction start: membership in a stage is inherited downward, since a stage is transitive, and a term's value lies in the stage, a constant because it was registered and a variable because the environment lies there.

The existential case is the one from the previous chapter. Downward, a witness from the stage is a witness in L, and the hypothesis transfers it. Upward is the case of closure: the truth of the existential in L is, by definition, the satisfiability the closure lemma consumes, so closure returns a witness already inside the stage, and the hypothesis applies to that one instead. Note which witness is used: not the one L happened to supply, but the one closure chose. That is why no circularity arises here, and why the stage never has to be a fixed point of anything.

The universal case is the existential case for the negated matrix, argued by contradiction. If some element of L failed the matrix, that failure would be a witness for the negated matrix, so closure would produce one inside the stage; but the hypothesis asserts that everything in the stage satisfies the matrix, a contradiction. Deciding whether the element fails is where the excluded middle enters the induction, and it is the only place.

Packaged, the theorem takes the formula and any ordinal the caller wants inside the stage, and returns a stage containing it. The extra ordinal is not a convenience: the certificate is not inherited by larger stages, so a caller cannot enlarge the stage afterwards to fit the set it is working with. It has to say up front what must fit, and the joint step carries it.

The package is sealed, and this is the seal that matters most in the book so far. Transparent, the stage it names unfolds through the joint step, the bounding lemma and the excluded middle at every rung; a consumer that mentions the stage in a type, as both consumers do, would drag that whole unfolding into every conversion check, and the next chapter simply does not finish. Sealed, the stage is a name, and the four things a consumer needs of it are the four the package already states.

The classical cost is unchanged: the excluded middle, in the descent, in deciding satisfiability, and once more in the universal case here. No choice, and no well-ordering of L.