Bounded alternatives to powerset that interpret ZFC

Question

In set theory, many properties/relations of interest can be expressed as $\Delta_0$ formulas (formulas with only bounded quantifiers):

\begin{align} \text{empty}(a) &\equiv \forall x \in a . \bot \\ \text{union}(a, b) &\equiv (\forall x \in b . \forall y \in x . x \in a) \land (\forall y \in a . \exists x \in b . y \in x) \\ \text{singleton}(a, b) &\equiv b \in a \land (\forall x \in a . x = b) \\ \text{pair}(a, b, c) &\equiv b \in a \land c \in a \land (\forall x \in a . x = b \lor x = c) \\ \text{subset}(a, b) &\equiv \forall x \in a . x \in b \\ \text{successor}(a, b) &\equiv b \in a \land \text{subset}(b, a) \land (\forall x \in a . x \in b \lor x = b) \\ \text{inductive}(a) &\equiv (\exists x \in a . \text{empty}(x)) \land (\forall x \in a . \exists y \in a . \text{successor}(y, x)) \\ \text{transitive}(a) &\equiv \forall x \in a . \forall y \in x . y \in a \\ \text{transitiveclosure}(a, b) &\equiv b \in a \land \text{transitive}(a) \\ \text{intersection}(a, b) &\equiv (\forall x \in b . \forall y \in x . ((\forall z \in b . y \in z) \to y \in a)) \land \forall y \in a . \forall x \in b . y \in x \end{align}

Thus several axioms of ZFC can be expressed in the form: \begin{align} \forall a_1 \ldots \forall a_n . \exists u . & \phi \end{align} where $\phi$ is $\Delta_0$. For example: \begin{align} \exists u . & \text{empty}(u) & \text{empty set axiom} \\ \forall a . \forall b . \exists u . & \text{pair}(u, a, b) & \text{pairing axiom} \\ \forall a . \exists u . & \text{union}(u, a) & \text{union axiom} \\ \exists u . & \text{inductive}(u) & \text{infinity axiom} \end{align}

There is, however, an odd one out: powerset.

\begin{align} \text{powerset}(a, b) \equiv \forall x . (\text{subset}(x, b) \to x \in a) \land (\forall x \in a . \text{subset}(x, b)) \end{align}

\begin{align} \forall a . \exists u . & \text{powerset}(u, a) & \text{powerset axiom} \end{align}

The powerset relation is not $\Delta_0$.

According to nlab:

When power sets don’t exist at all, whether as a set or a proper class, this results in strictly weaker foundations, since in this case one simply cannot form various mathematical structures which require the use of power sets, such as the Dedekind real numbers, topological spaces, frames, and locales. This is usually the case for predicative mathematics done internally in a Heyting or Boolean pretopos, as well as for predicative material set theories like Kripke–Platek set theory which do not have an internal notion of class. In dependent type theory, this notion of predicativity requires not having any type universes in the type theory itself, since otherwise $\sum_{A:U} \text{isProp}(A)$ is a large type of propositions. In addition, unlike for set theory, not having power sets in dependent type theory results in additional structure like formal topologies or inductive covers not being definable in the type theory, since without universes or types of propositions one cannot define relations between elements and subtypes.

My question is as follows: Let ZFC^- be the axioms of ZFC without powerset, as described in [1]. Let A be an axiom of the form $\forall a_1 \ldots \forall a_n . \exists u . \phi$ where $\phi$ is $\Delta_0$, such that ZFC^- + A is consistent and interprets ZFC. Are there any examples of such A, in the literature or otherwise? If so, what are they?

References:

1. What is the theory ZFC without power set?
2. What would remain of current mathematics without axiom of power set?

Answer 1

The answer is Yes. The simple fact is that it is much easier to interpret ZFC from low-complexity assertions than one might expect. For example, even PA+Con(ZFC) can already interpret ZFC, since one can define the tree of attempts to build a complete consistent Henkin theory extending ZFC and then interpret via the Henkin model arising from the leftmost branch through this tree.

In your case, therefore, we can take $A$ as the arithmetic sentence Con(ZFC), which has much simpler set-theoretic complexity than you request, and then $\text{ZF}^-+A$ will be consistent relative to ZFC+Con(ZFC), and it will interpret ZFC via this Henkin model construction.

Perhaps a somewhat more natural $A$ would be: "there is an ordinal $\alpha$ for which $L_\alpha\models\text{ZFC}$, where $L_\alpha$ is as in the constructible hierarchy. This can be expressed in a $\Sigma_1$ manner, and so it has the desired logical complexity, and it enables an interpretation of ZFC.

Update. But finally, let me consider the question whether there is such a principle $A$ as you request, with the further requirement that it is a theorem of ZFC. That is, we want $A$ to be a theorem of ZFC of complexity $\Pi_2$ for which $\text{ZFC}^-+A$ interprets ZFC.

For this, I claim, the answer is no. The reason is that for such an $A$, I claim that ZFC proves $\text{Con}(\text{ZFC}^-+A)$, and this would mean that the theory $\text{ZFC}^-+A$ could not interpret ZFC without proving its own consistency, in violation of the incompleteness theorem.

To see that ZFC proves $\text{Con}(\text{ZFC}^-+A)$, we observe first that ZFC proves that $\text{ZFC}^-$ holds in the structure of hereditarily countable sets HC, also commonly denoted $H_{\omega_1}$. This is the set of all countable sets, whose members are countable, and members of members, and so forth — the transitive closure of the set should be countable. Next, we observe that if $A$ is true, then it is true in HC. This amounts essentially to the Lévy reflection theorem, asserting $\text{HC}\prec_{\Sigma_1} V$. The reason at heart is that if $\forall \vec x\exists y\phi(\vec x,y)$, where $\phi$ is $\Delta_0$, then for all hereditarily countable $\vec x$, one can find a hereditarily countable $y$ witnessing $\phi(\vec x,y)$. The reason is that one can take any witness $y$, form a countable elementary substructure containing $\vec x$ and $y$. The Mostowski collapse will preserve the $\vec x$ and move $y$ to a hereditarily countable witness of $\phi$. Thus, HC already satisfies $A$, as desired.

So ZFC proves that there is a model of $\text{ZFC}^-+A$, namely HC or indeed $H_\kappa$ for any regular $\kappa$, and this prevents this latter theory from interpreting ZFC.