Q:

Is the top-down approach to universe-juggling mathematical consistent?

Here's an idea I've been sitting on for awhile. I guess it's time to expose it to the flaming sword of expert opinion. Not sure if it will remain standing by the end of this - oh well. Here goes nothing.
The default way of thinking about set-theoretic universes is (arguably) that there's a set $U_0$ of small sets, which is an element of a larger universe $U_1$ of slightly less small sets, which is included in a larger universe of yet less small sets, etc. We end up with a sequence $$U_0 \in U_1 \in U_2 \in \ldots$$ that's probably best regarded as ordinal-indexed. Let's call this the bottom-up approach.
However for the purposes of universe-juggling, it would be more convenient to start at the top, and just deal with (unqualified) sets for as long as we can. Then when we need to do some juggling, we move from the whole universe to a smaller subuniverse $U_0$ whose elements are thought of as "small sets". If we need another level of the hierarchy, we deal with the elements of a yet smaller universe $U_1$ which is thought of as the universe of very small sets. Thus we end up with a sequence $$U_0 \ni U_1 \ni U_2 \ni \ldots.$$ Let's call this the top-down approach.
If I understand correctly, the bottom-up approach is believed to be mathematically consistent; in particular, if our definition of "universe" is "a set $U$ such that $|U|$ is a strongly inaccessible cardinal and $(U, \in \restriction_U)$ is elementarily-equivalent to the the cumulative hierarchy $V$", then the bottom-up approach is equivalent to a moderately strong large cardinal axiom. I think it's equally as strong as "there exists a proper class of strongly Mahlo cardinals" (can an expert comment on this?)
I'm not sure the top-down approach is consistent, which is a shame since it's the approach I prefer. At first-blush it seems to contradict the axiom of regularity and in particular the well-foundedness theorem. However, I think we can save the approach by just being careful to make sure the internal language cannot actually see the full sequence $n \in \mathbb{N} \mapsto U_n$. In particular, if our approach to axiomatizing is to include a constant symbol $U_n$ for each $n \in \mathbb{N}$, while avoiding the axiom "for each $n \in \mathbb{N}$ there exists an $n$-long sequence of universes $U_0 \ni \cdots \ni U_n$" it seems possible that the threat of contradiction can be averted.

Question. Is the top-down approach to universe-juggling mathematical consistent? If so, what is its consistency strength?

A:

One first stab at this would be to look at the following theory: we take the language of set theory together with new constant symbols $\kappa_i$ for each $i\in\mathbb{N}$, and look at the theory gotten from ZFC by:

extending the Separation and Replacement schemes to formulas in the new larger language;
adding for each $i\in\mathbb{N}$ the sentence $\kappa_i\ni\kappa_{i+1}$; and
adding for each $i\in\mathbb{N}$ the scheme saying that $V_{\kappa_i}\prec_{\{\in\}\cup\{\kappa_j: j>i\}} V$. (That is, for each $i\in\mathbb{N}$ and each $\varphi$ in the language $\{\in\}\cup\{\kappa_j:j>i\}$, we add the axiom "$\varphi\iff\varphi^{V_{\kappa_i}}$.")

I believe this will suffice for your purposes. And unless I'm making a silly mistake this is consistent as long as for each $i, j\in\mathbb{N}$, ZFC + "there is a tower of length $i$ of $\Sigma_j$-elementary submodels of the universe" is consistent, which is fairly mild by large cardinal standards.
Similarly, we could get $\mathbb{Q}$-many universes, or ...

In fact, a bit more compactness juggling gives (under appropriate consistency hypotheses of course) a model $M$ of ZFC in which the set of $M$-ordinals $\alpha$ with $(V_\alpha)^M\prec M$ is cofinal in $Ord^M$ and has ordertype exactly $\mathbb{Q}$. In some sense this is the extreme example: the universes are as homogeneously and plentifully arranged as possible and the model itself is small so amenable to silly external combinatorics.

