# Top-Down Recognition of Superstructure Stages

Concerning the unusual way, just hinted at, of approaching the cumulative hierarchy, one might contend that it is presumably harder—or, if anything, less transparent—to infer directly from the definition of V(L) a statement such as

than to prove, for any pair a, в of ordinals, the biimplications

A tentative reply is that transfinite induction of the kind schematized in Fig. 10.3 (left) is often a shortcut compared to a proof pattern relying on the theory of ordinals. On a smaller scale, as will now be seen, we can treat superstructures without numbering their stages: with virtually no recourse to natural numbers.15

We can exploit recursion to describe sets L which are stages of a superstructure. The first of the three definitions shown below is e-recursive and specifies a function seeking a set s of individuals (recall Sect. 10.2) such that sm = L for some m e N; if such an s exists, it can be found by repeated extraction

of the ‘logarithm’ of L, where ? = log L momentarily means that L = ? U P (?) (needless to say, this equation has either one or no solution—in the former case, 0e L and hence L cannot be regarded as a set of individuals):

basis(L) =Def if 0 e L & L П U L = 0 then L

elseif (3 ? | L = ? U P (?) & P (?) П U(? P (?)) = 0) then arb ({basis(?) : ? e L | L = ? U P(?)}) else {0} fi ;

Stage(L, 5) ^ef L = 0 v (basis(L) = S & S = {0}) ;

The chain L = L0, Ln+1 = log Ln of logarithms surely has finite length but may end with a set Lm such that either 0e Lm or Lm П U Lm =0 holds, in which cases Lm cannot serve as a set of individuals. When this happens, basis(L) will flag the failure by returning {0}; but failure can be detected earlier during the descent, should P(Ln) П U (Ln P(Ln)) be nonnull at some point. The predicate Stage(L, S) indicates L as a potential stage of the superstructure—if any—generated by its ‘ultimate logarithm’ S = basis(L) when the latter is obtained without failure; but even when so, S does not qualify as a set of individuals unless one can indefinitely ascend, starting with S, through stages none of which reveals the inner structure of its elements. The property Ur (S) captures the sense of our last remark.

Under the assumption Ur (s0), we have in fact checked with the assistance of Ref that s behaves as desired (see Fig. 10.5), even though genuine individuals (‘ure- lemente of the nature set forth in [14, p. 11]) do not exist in the von Neumann cumulative universe of all sets.

The interface, shown in Fig. 10.5, of the Theory superstructure may look intimidating, the cause being that it exploits the property (3? | Stage(?, s0) & X e ?) [1]

Fig. 10.5 Interfaces of the Theorys of universes and superstructures

as a temporary surrogate of the sought s0. Only its final claim shows that the X’s enjoying that property form a set, namely the output parameter sstr0 to be then actualized as s outside the Theory; even so we can exploit the said property as a universe to get, through the Theory universe, derived closure properties. Observe, in fact, that the second-to-last and penultimate claim of superstructure match the assumptions of universe and its internally derived conclusions.

The moral is that our recursive characterization of the stages of a superstructure disclosed handy patterns to our formal reasoning about them; however, at one point we had to resort to a construction from below, closer in spirit to [14, Sect. 1.3]: this happened when it came to ascertaining that the union-class of all the stages is, in fact, a set. For that purpose, we applied the Theory reachGlob (see Fig. 10.2 above) to the actual input parameter if X = 0 & s0 =0 then s0 else X U P (X) fi, thus getting a function glob whence the sought superstructure was obtained simply by taking sstr0 = U glob(0). The following triad of equations conveys the idea, in functionally equivalent terms:

These equations, in fact, adjust the construction of Fig. 10.4 to the case at hand; as said under that figure, is a Ref’s built-in witnessing that infinite sets exist.

• [1] Natural numbers will play an irreplaceable role in the informal arguments providing the rationalefor the formal constructions that follow; within the formal treatment, their collection N will act asa set whose infinitude is easiest to prove (and infinite sets will be crucial in Sect. 10.8).