Work in a theory where the primitives are classes $X,Y,Z,\dots$, and class membership $X\in Y$, and add an individual constant $\mathcal{M}$ called 'the multiverse'. Classes $V$ which are members of the multiverse, that is such that $V\in\mathcal{M}$, are called universes. Classes which are members of some universe are called sets, denoted by lowercase letters $x,y,z,\dots$. If we say that a class $X$ is a $V$-set for some fixed universe $V$, we mean that $X\in V\in\mathcal{M}$.
We have axioms as follows:
Extensionality, in the usual sense applied to classes.
Class Separation, asserting that for any predicate $\phi(\cdot,Y)$ where $Y$ stands for any finite number of class parameters, and for every class $Z$, there exists a class $A$ whose members are exactly those members of $Z$ satisfying $\phi(\cdot,Y)$. We use this implicitly in the usual way, writing $$\{X\in Z:\phi(X,Y)\}$$ for the class $A$ guaranteed by the instance of this axiom scheme for a predicate $\phi(\cdot,Y)$ and class $Z$ as above.
Define $\emptyset=\{V\in\mathcal{M}:V\neq V\}$.
- Class Pairing, asserting that for any two classes $X,Y$ there exists a class $Z$ whose members are $X$ and $Y$. $$\forall X\forall Y\exists Z(A\in Z\iff A=X\vee A=Y).$$ As usual, we write the class $Z$ guaranteed by this axiom and two classes $X,Y$ as $\{X,Y\}$.
For classes $X,Y$, define $\{X\}=\{X,X\}$ and $(X,Y)=\{\{X\},\{X,Y\}\}$ as usual.
- Class Cartesian Product, asserting that the Cartesian product of any two classes exists. $$\forall X\forall Y\exists Z\big(A\in Z\iff\exists X'\in X\exists Y'\in Y\big(A=(X',Y')\big)\Big).$$ As usual, we write the class $Z$ guaranteed by this axiom and two classes $X,Y$ as $X\times Y$.
For classes $X,Y$, define a relation from $X$ to $Y$ to be a subclass of $X\times Y$ as usual and define a relation on $X$ to be a subclass of $X\times X$ as usual.
Universes are Models, asserting that each member of the multiverse consists of an ordered pair $(V,\in_V)$ where $V$ is a class, called a universe$^*$, and $\in_V$ is a relation on $V$ called membership in $V$. $$\forall X\Big(X\in\mathcal{M}\implies\exists(V,\in_V)\big(X=(V,\in_V)\wedge\in_V\subseteq V\times V\big)\Big).$$ We will abuse notation and denote a member $(V,\in_V)\in\mathcal{M}$ of the multiverse by its first coordinate $V$ ($^*$bringing us into alignment with the terminology and notation defined in the heading). Call a universe standard iff membership in that universe is actual membership. $$V\ \text{is standard}\iff\forall x,y\in V(x\in_Vy\iff x\in y).$$ Call a universe transitive iff it is transitive in the usual sense, and complete iff it is transitive and contains all subsets of its members as members. $$V\ \text{is transitive}\iff\forall X\forall Y(X\in Y\in V\implies X\in V),$$ $$V\ \text{is complete}\iff\Big(V\ \text{is transitive}\wedge\forall X\forall Y(X\subseteq Y\in V\implies X\in V)\Big).$$ We use the word 'models' in the usual sense; a universe $V$ models a predicate $\phi$, written $V\models\phi$, iff relativizing $\phi$ to $V$ and replacing every instance of $\in$ in $\phi$ with $\in_V$ yields a true sentence (so if a standard universe models a sentence it is 'externally' true as well as 'true in that universe').
Internal Empty Set, asserting that every universe thinks it has an empty set. $$\forall V\in\mathcal{M}\big(V\models(\exists z\forall x(x\notin z)\big).$$
Standard Universe, asserting that a standard universe exists. $$\exists V\in\mathcal{M}(V\ \text{is standard}).$$ Note that $(6.)$ implies that all standard universes actually have the empty class as a set.
For the final axiom, we refer to the class theory given by the primitives above and axioms $(1.)-(7.)$ as $T_\emptyset$. For a fixed universe $V$ say that a predicate $\psi$ is safe above $V$ iff the multiverse doesn't occur in it and no universes containing $V$ as a subclass occur in it (including $V$), and let $\Phi_V$ denote the class of all predicates safe above $V$. Then we have
8. Truth Closure. For every universe $V$ and every predicate $\phi$ which is safe above $V$, if $V$ modeling $\phi$ is independent of $T_\emptyset$ then there exists a universe $V+\phi$ modeling $\phi$ such that $V$ is an elementary submodel of $V+\phi$. $$\forall V\in\mathcal{M}\forall\phi\in\Phi_V\Big(T_\emptyset\nvdash(V\models\phi)\wedge T_\emptyset\nvdash\neg(V\models\phi)$$ $$\implies\exists V+\phi\in\mathcal{M}(V+\phi\models\phi\wedge V\prec V+\phi)\Big).$$
This should give us universes with any axioms we could possibly want by starting with our very weak empty set universes and observing that their modeling anything is independent of the first four axioms, but I can't tell if this is even a legitimately phrased axiom (or if it is wether it blows the consistency strength all the way up to inconsistent).
Question 1. Is this a legitimately phrased axiom, and if so is it obviously inconsistent?
At least one issue is that we don't want to keep referring to $T_\emptyset$ when formulating truth closure, we want to recursively refer to $T_\emptyset$ together with the axioms stating that various universes model various predicates that we've already added at previous stages, but it's not clear how to state this formally (or if this is a legitimate axiom scheme formulation). I also can't tell if we want to assert that we have standard/transitive/complete universes for each predicate safe above and independent of a given universe; I suspect that we at least want to assert a standard one, but completeness/transitivity seem like they might conflict with some of the predicates we might want to 'add' to the new universe.
If this last axiom can't be fixed, we could use the following axioms instead -- they seem to give a more limited multiverse 'centered around $ZFC$', but I'm more confident that they're legitimately phrased and not obviously inconsistent.
Let $\mathscr{L}_\alpha$ denote the $\alpha^{th}$ order language of class theory with identity on the first sort. For each universe $V\in \mathcal{M}$ say that a predicate $\psi$ is $\alpha^{th}$-order $V$-safe iff $\psi$ is expressed in $\mathscr{L}_\alpha$ and only contains $V$-set parameters and no universes occur in $\psi$, and also $\mathcal{M}$ does not occur in it. Further, use the standard definitions of when a predicate is $\Sigma_n$ or $\Pi_n$. Say that a predicate $\psi$ is $V$-safe iff it is $\alpha^{th}$-order $V$ safe for some $\alpha$. Then the axioms are extensionality and class separation as above, together with
3*. Completeness for Universes, asserting that all members of $\mathcal{M}$ are closed under their member’s members and member’s subsets. $$\forall V\in\mathcal{M}\big((Y\in X\in V\implies Y\in V)\wedge(Z\subseteq X\in V\implies Z\in V)\big).$$
4*. Varied Set Existence, asserting that for any universe $V\in\mathcal{M}$ and any $1^{st}$-order $V$-safe parameter free predicate $\phi$, if all the classes for which $\phi$ holds are $V$-sets then the class of these sets is a $V$-set. Further, for each ordinal $\alpha$ and pair of ordinals $n,m\leq\omega$ there exists a universe $V_{\alpha,n,m}$ such that for any $\alpha^{th}$-order $V_{\alpha,n,m}$-safe predicate $\phi(\cdot,y)\in\Sigma_n\cup\Pi_m$, where $y$ stands for any finite number of $V_{\alpha,n,m}$-set parameters, if all the classes for which $\phi(\cdot,y)$ holds are $V_{\alpha,n,m}$-sets then the class of these sets is a $V_{\alpha,n,m}$-set.
5*. Optional Regularity, asserting that if we have a universe $V$ where regularity is independent of the axioms present relativized to that universe then there exists a universe $V^{Reg}$ with the same axioms as $V$ plus regularity and there exists a universe $V^{\neg Reg}$ with the same axioms as $V$ plus anti-regularity.
6*. Optional Choice, asserting that if we have a universe $V$ where choice is independent of the axioms present relativized to $V$ then there exists a universe $V^{Ch}$ with the same axioms as $V$ plus choice and a universe $V^{\neg Ch}$ with the same axioms as $V$ plus the negation of choice.
The motivation for these axioms is populating the multiverse with some of the canonical universes we care about; $ZFC$ will be $V_{1,\omega,\omega}$, $V_{n,\omega,\omega}$ for $1<n<\omega$ will have indescribable cardinals as described here (where it is also mentioned by Joel that $V_{\alpha,\omega,\omega}$ for $\omega\leq\alpha$ will have strongly unfoldable cardinals). Further, the $V_{1,n,m}$'s for $n,m<\omega$ should be weak set theories but I'm not familiar enough with set theories weaker than $ZF$ to comment on what interesting consequences we might have. We are being loose mixing theories and models of those theories; by saying that $V_{1,\omega,\omega}$ 'is $ZFC$', we mean that the theory obtained by relativizing all axioms here to $V_{1,\omega,\omega}$ 'is' ZFC (in the same sense as in A. Lévy, R. Vaught, Principles of partial reflection in the set theories of Zermelo and Ackermann).
The goal is to obtain one class theory that allows for a simultaneous consideration of all 'set theories' and the relationships between them, in a 'multiverse' sense as proposed in Hamkins, The set-theoretic multiverse. In particular, things like
Forming a (double? higher?) category of universes ${\bf Uni}$ with ${\bf Ob}_{\bf Uni}=\mathcal{M}$ and arrows $V\to V'$ given by forcing extensions from $V$ to $V'$,
Starting with a universe $V$ and taking the 'forcing closure' $F(V)\subseteq\mathcal{M}$ consisting of all universes that can be obtained form $V$ by forcing,
and the like should be possible in this theory (other relationships like being an elementary submodel, a ground, a mantle, etc. should also be formalizable, perhaps providing vertical/horizontal arrows or arrows between arrows in ${\bf Uni}$).
This came up while reading through Lévy and Vaught's paper linked above -- they essentially view Ackermann's class theory concentrated on his individual constant $V$ to be 'set theory', and show that any theorem about sets in standard set theory also holds relativized to $V$ in Ackermann's theory.$^1$
Initially my thought was 'why not just specify an infinitude of individual constants $V,V',V'',\dots$ and treat them as separate set-theoretical universes with different axioms, then explore their relationship in this setting', but it wasn't clear how to write down axioms saying that
'for each possible collection of set theoretical axioms $\{\phi_i\}_{i<\alpha}$ dictating a set theory $T$, there exists an individual constant $V_T$ called the 'universe of $T$ sets' with axioms $\{\phi_i^{V_T}\}_{i<\alpha}$'
without running into issues of consistency, since trivially some collections of axioms give set theories that are inconsistent and allowing these universes into the multiverse collapses it (unless I'm mistaken). We could insert the word 'consistent' between 'possible' and 'collection' above, but I'm still not sure how to formally codify this as an axiom scheme.
The eventual workaround was a single individual constant $\mathcal{M}$ for the multiverse whose members are universes together with axioms to populate $\mathcal{M}$ as presented above, but I am not well versed enough in forcing or other research level set-theoretic constructions to know if this axiomatization is legitimate or sufficient.
Question 2. Do either of the above suggestions work to axiomatize the multiverse, in the sense that we can reproduce all the constructions we care about between universes of sets? If not, can we modify the above axiom list to yield a class theory that does work?
Any assistance is appreciated. There have been questions asked about similar topics before on MO, but I think this one is different enough to avoid being a duplicate.
$^1$Although Reinhardt, Ackermann's set theory equals ZF famously showed that Ackermann's original theory is equiconsistent with $ZF$, a modification laid out in F. A. Muller, Sets, Classes and Categories very close in spirit to the second axiom list above is claimed to be stronger in consistency strength and thereby avoids the philosophical position that 'all classes in Ackermann's theory are really just sets'. Of course these classes can be modeled as sets by adding a large cardinal axiom $\phi$ to $ZFC$, but if we can also add $\phi^V$ to Ackermann's modified theory and obtain something stronger in consistency strength than $ZFC+\phi$ we will always have new classes that 'aren't sets' even when we try to use large cardinals to 'make everything a set'.