存在論理式の構成可能段階への反映

It can be done, and the argument is Montague's. Fix a matrix and an environment of parameters. If a witness exists at all, there is a least stage containing one, and that stage is a set-sized answer to a class-sized question. Range over all tuples of parameters drawn from one stage, bound the answers, and the result is a single stage that answers for every tuple from the stage below. Iterate that step through the natural numbers and take the union: the limit answers for its own parameters, because any finite tuple from the limit already lies in some finite layer, whose answers were bounded at the next.

Two departures from the usual practice occur here. The choice of witness is where a well-ordering of L is normally invoked, and it is not needed: what the argument requires is a canonical ordinal, not a canonical element, and the ordinals are already well-ordered by membership. So the least stage that holds a witness is taken directly, by the descent of the stage chapter, without deciding which witness is there. And the parameters are a tuple from the start. Writing the one-parameter case first and generalizing later would mean writing the whole construction twice, since every step of it is indifferent to how many parameters there are; the only place the tuple matters is in locating it, where finitely many layers have to be merged into one.

An environment lies below a stage when each of its entries does. Reading the tuple of indices back off such an environment is the inverse operation, and it returns the equation as well, since the construction will need to know that the environment it bounded is the one it was given. The equation is where constructibility being a proposition is used: two elements of the model agree as soon as their underlying sets do.

Totality then wants a value even when no witness exists, and the excluded middle supplies the case distinction. As in the stage chapter, the distinction is made by an explicit auxiliary rather than by a with, because the load-bearing lemma below has to name the very same decision value and match on it.

And the property the whole construction rests on: if the environment is satisfiable at all, its answering stage really does hold a witness. The proof has to know which branch the decision took, and it cannot ask, because the decision is a value of the excluded middle and nothing computes it. So it does the standard thing: quantify over the branch, remember the equation that the branch is the decision, and transport along it. In the false branch the hypothesis refutes itself.

Stating the reach with the gap as an explicit summand, rather than through an order relation, is what makes two rungs mergeable by addition alone. That matters because merging rungs is the only thing a tuple of parameters costs, and it is worth not paying for arithmetic to do it.

Separating the ladder from the tower is worth a moment's care, because the next chapter needs a ladder built differently: one whose single step closes all the matrices of a formula at once. Everything below is proved of the ladder, so that chapter builds its ladder and gets the argument, rather than running it again.

The closure argument needs its parameters on a rung, not merely under the limit. For one parameter, two inversions get it there: an ordinal in the limit belongs to one of the sets being unioned, hence to a rung; and a set in the stage of the limit belongs, by the tower's characterization, to the operator applied to the stage of some smaller ordinal, so locating that ordinal and going back in places the set in that rung's stage.

For a tuple, the rungs found for the entries have to be merged, and the reach lemma merges two of them: from rungs n and m, both reach rung suc (n + m), one of them directly and the other after commuting the sum. Recursion on the tuple merges all of them, and monotonicity carries the earlier entries up.

Given it, the limit is closed for the matrix. Locate the environment on a rung and name it there: it is the image of some tuple of indices of that rung's stage, up to an equality that the reading lemma returns along with the tuple. Its answering stage is on the next rung, so whatever lives in the answering stage lives in that rung's stage, hence under the limit; two applications of monotonicity, and the equation transported back.

This gives the theorem that later chapters use. For an environment under the limit, the class model satisfies the existential exactly when a witness lies in the limit's stage. Forwards is closure; backwards is forgetting where the witness lives.

The forward direction needs no translation step, because the two sides are the same proposition already: the semantics of an existential quantifier is the truncated sum over the carrier, and that is what SatEx was defined to be. So the theorem is closure with its statement rewritten, and moving between syntax and the meta-level requires no further work.

The step is sealed. Unfolded, it is a bound built from a bound built from the excluded middle, and the closure argument matches on rungs repeatedly; a transparent definition would push that whole tower into every conversion check. The three properties open the seal once each, and the last of them is the one place transitivity is used, so the chain from the answer through the bound into the step is closed inside the seal and the caller sees only its conclusion.

The construction used the excluded middle twice, once to decide satisfiability and once inside the descent, and used the axiom of choice not at all. That is the point of taking the least stage rather than the least witness: the ordinals come well-ordered, and nothing here has to ask for a well-ordering of L.

What this chapter achieves is one quantifier, with any number of parameters. An arbitrary formula may contain many quantifiers, hence many matrices, and no limit taken for a single matrix covers them all; the next chapter builds a ladder whose step closes all of them at once, and thereby obtains everything above directly, without redoing any of the individual arguments.