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 supertransitive 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 supertransitive}\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 about members of that universe 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\big(\exists z\forall x(x\notin z)\big)\Big).$$
Standard Transitive Universe, asserting that a standard transitive universe exists. $$\exists V\in\mathcal{M}(V\ \text{is standard and transitive}).$$ Note that $(6.)$ implies that all standard transitive 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$ whose existence is not instantiated by this axiom and every predicate $\phi$ which is safe above $V$, if $V$ modeling $\phi$ is consistent with $T_\emptyset$ then there exists a universe $V+\phi$ modeling $\phi$ such that $V$ is an elementary submodel of $V+\phi$. For every universe $V’$ instantiated by $n$ applications of this axiom at universes $\{V+\sum_{i<m}\phi_i\}_{m<n}$ and statements $\{\phi_i\}_{i<n}$, so $V'=V+\sum_{i<n}\phi_i$, denote by $T_\emptyset^{V’}$ the theory given by $T_\emptyset$ plus individual constants $\{V+\sum_{i<m}\phi_i\}_{m\leq n}$ and axioms stating that $V'=V+\sum_{i<n}\phi_i$, that $V+\sum_{i<m}\phi_i \in\mathcal{M}$ for all $m\leq n$, that $V+\sum_{i<m}\phi_i\preceq V+\sum_{i<m+1}\phi_i$ for all $m<n$, and that $V+\sum_{i<m}\phi_i \models\bigwedge_{i<m}\phi_i$ for all $m\leq n$. For any statement $\phi’\in\Phi_{V’}$, if $V’$ modeling $\phi’$ is consistent with $T_\emptyset^{V’}$ then there exists a universe $V’+\phi’$ modeling $\phi’$ such that $V’$ is an elementary submodel of $V’+\phi’$.
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 seven 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 may want to assert that we have standard/transitive/supertransitive 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 (super)transitivity seems like it may conflict with some of the predicates we might want to 'add' to the new universe.
In particular, $V_\omega$ with an appropriately defined $\mathcal{M}$ is a model of $T_\emptyset$ which allows ‘universes’ with almost nothing in them, while the universe $\mathbb{V}$ in MK (for example) with $\mathcal{M}$ appropriately defined is also a model of $T_\emptyset$ where universes can be quite robust —- these together show that almost all statements we can write down about the standard transitive universe asserted to exist in axiom $(7.)$ are independent of $T_\emptyset$, giving us many more universes via axiom scheme $(8.)$.
In order to truly 'keep everything in house' when constructing these models, we also have
- Standard Theories. For any well-established set theory $T$ (for example all variants of $ZFC$ with/without large cardinals, NF, KP, etc.) let $T_\wedge$ denote the conjunction of all axioms of $T$; then there exists a supertransitive universe $V_T$ such that $$V_T\models T_\wedge.$$
If these last two axioms aren’t legitimately phrased and 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*. Supertransitivity 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'.
After posting this question and not immediately being dunce capped, I decided to take this theory more seriously and uploaded a short note to the arxiv expanding on it, with some additional proposed axioms to 'structure the multiverse' and allow us to consider 'multiversal category theory'.
Edit:
In response to Mikhail's comment below, in non-technical terms what I'd like to accomplish is a 'maximally powerful theory of the multiverse' in the consistency strength sense of power, which is also 'maximally permissive' in terms of what kinds of universes it allows for, and which is 'ontologically clean' in the sense that its power is derived from axioms which come as close as possible to directly capturing intuition for what a multiverse 'should' contain, with minimal extra technical jargon introduced to capture this intuition. (I make no claim to have done a good job at accomplishing any of these goals.)
In response to James E Hanson's two comments, I intended for the 'safe above' clause to prevent us from referring to a whole universe in the predicate we use to apply truth closure -- both of your examples explicitly use a symbol to refer to the whole universe. I think saying that the universe is standard accomplishes your 'is the real' part of the predicate, so it may be best to omit the requirement that the new universes instantiated by truth closure be standard.