Below I'll re-iterate the exposition [with modification to suit this question] of a theory of mine given on Mathoverflow lately, which is unsolved yet. Howevere, here, I want to understand the matters of how should one go about proving the consistency of such system by dropping some features of it. First I'll present the modified exposition:
Exposition
The idea of this question is if we can go in the direction opposite to that of Cantor's argments for sets being strictly smaller than their powers, through building two disjoint hierarchies on top of two distinct empty objects, then we add an axiom saying that for every object in one hierarchy there is an object in the other hierarchy with an isomorphic set picture (i.e. the $\in$ graph on its inclusive transitive closure), the question is:
Can we add a bijective function $J$ over some infinite stage of the first hierarchy to the power set of its $\in$-copy in the second hierarchy, and restrict Replacement axioms of both hierarchies to work over formulas [not using $J$] coming from parameters restricted to the the union of both hierarchies with all quantifiers relativized to that union?
Formal workup
Language: $\mathsf {FOL} (=, \in, \emptyset, \varnothing, J)$
$\emptyset, \varnothing$ are constants; $J$ is a partial function symbol.
Axioms: those of ID theory +
- Weak Extensionality: $\forall x (x \in a \iff x \in b) \land \exists x \, (x \in a) \to a=b$
Define: $set(y) \iff \exists s (y \in s)$
Comprehension: $\exists x \forall y (y \in x \iff \phi(y) \land set(y))$, if $\phi$ doesn't have $x$ free.
Emptyness: $\forall x: \not \exists y \, (y \in x) \iff x=\emptyset \lor x= \varnothing$
Sets existence: $set (\emptyset), set(\varnothing), \emptyset \neq \varnothing$
Define: $x \text{ is } \ _\emptyset set \iff set(x) \land \forall y \in TC(x) [\emptyset \in TC(\{y\})] \land \varnothing \not \in TC(\{x\})$
Define: $x \text{ is} \ _\varnothing set \iff set(x) \land \forall y \in TC(x) [\varnothing \in TC(\{y\})] \land \emptyset \not \in TC(\{x\})$
Where $TC$ stands for 'transitive closure' defined in the usual manner.
Define: $\ _\emptyset V = \{x: x \text{ is } \ _\emptyset set\}$
Define: $\ _\varnothing V = \{x: x \text{ is } \ _\varnothing set\}$
Pairing: $ a,b \text { are } \ _\emptyset sets \to set ( \{a,b\} ) \\ a,b \text { are } \ _\varnothing sets \to set ( \{a,b\} )$
Union: $set(x) \to set(\bigcup x)$
Power: $ \ _\emptyset set(x) \to set(\ _\emptyset \mathcal P(x)) \\ \ _\varnothing set(x) \to set(\ _\varnothing \mathcal P(x)) $
Where: $\ _\emptyset \mathcal P (x) = \{set(y): \forall z \in y (z \in x) \land y \neq \varnothing \} ; \\\ _\varnothing \mathcal P (x) = \{set(y): \forall z \in y (z \in x) \land y \neq \emptyset \} $
Infinity: $set (_\emptyset \omega);set (_\varnothing \omega) $
Replacement: if $f$ is a definable function by a formula [not using $J$] with all quantifiers relativized to $ \ _\emptyset V \ \cup \ _\varnothing V$ , with parameters from $\vec{p},a$, then: $$\forall \vec{p},a \in \ _\emptyset V \ \cup \ _\varnothing V :\\ \forall x \in a (f(x) \in \ _\emptyset V) \lor \forall x \in a (f(x) \in \ _\varnothing V) \\\to set(\{f(x): x \in a\})$$
Copying: $\forall x \in \ _\emptyset V \exists y \in \ _\varnothing V \exists f \ ( f: picture(x) \approx picture(y))$
Where the picture of a set $x$ is the $\in$-graph on the transitive closure of $\{x\}$; $`` \approx "$ stands for "isomorphism" on membership.
The copying relation shall be denoted using $``^*"$, so for every $x \in \ _\emptyset V$, we define $x^*$ as the element of $\ _\varnothing V$ whereby an isomorphism $f$ exists from the set picture of $x$ to the set picture of $x^*$. We call $x^*$ as the $\in$-copy of $x$.
Define recursively: $$ \ _\emptyset V_\emptyset = \emptyset \\ \ _\emptyset V_{\ _\emptyset \alpha + 1} = \ _\emptyset\mathcal P (V _{_\emptyset \alpha}) \\ \ _\emptyset V_{\ _\emptyset \lambda} = \bigcup_{\alpha \in \ _\emptyset \lambda} \ _\emptyset V_\alpha $$, for limit $_\emptyset \lambda$
Similarly define $\ _\varnothing V_{\ _\varnothing \alpha}$ by replacing $\emptyset$ by $\varnothing$ in the above definitions.
- Foundation: $$\ _\emptyset V = \bigcup_{\alpha \in \ _\emptyset \mathsf {ORD}} \ _\emptyset V_\alpha \\ \ _\varnothing V = \bigcup_{\alpha \in \, _\varnothing \mathsf {ORD}} \ _\varnothing V_\alpha $$
Where $\alpha \in \ _k \mathsf{ORD}$ iff $\alpha$ is a transitive $ _k set$ of transitive sets, having every nonempty subclass of it having a least element with respect to $\in$; where $k \in \{\emptyset, \varnothing\}$
- Anti-Cantorian: $$\exists \text{ limit } \ _\emptyset \alpha \, ( J: \ _\emptyset V_{\ _\emptyset \alpha} \rightarrow \ _\varnothing \mathcal P ((\ _\emptyset V_{\ _\emptyset \alpha} )^*),\\ J \text{ is a bijection })$$
So the difference between the system as exposited here and that at MO, is that here $J$ is not allowed to be used in Replacement.
Is this system consistent?
Let $\sf ZFC^{\emptyset,\varnothing}$ be the theory $\sf ZFC - Ext. + Weak \ Ext. + \forall x (empty(x) \iff x=\emptyset \lor x=\varnothing)+ \\ \emptyset \neq \varnothing$
Where $\sf Weak \ Ext.$ is Extensionality for nonempty sets.
It is known that this theory is consistent.
The two hierarchies are easily raised here.
Working in $\sf ZFC^{\emptyset, \varnothing}$ + there exists a well founded transitive model of $\sf ZFC^{\emptyset, \varnothing}$:
Take a countable well-founded transitive model $\cal M$ of $\sf ZFC^{\emptyset, \varnothing}$, and $(\mathcal P (\mathcal M) , \in^{\mathcal P (\mathcal M)})$ would be a model of this theory