# Can power set axiom be proved in a class theory of well ordered hereditarily accessible sets?

I'll repost this question here:

Working in a pure class theory, where sets are defined as elements of classes. That is:

Define: $$set(x) \iff \exists y (x \in y)$$

Let's have the following known three axioms from $$\text{MK}$$

Extensionality: $$\forall x\forall y [\forall z (z \in x \leftrightarrow z \in y) \to x=y]$$

Class Comprehension: if $$\varphi$$ is a formula in which the symbol $$x"$$ is not free, then $$(\exists x \forall y (y \in x \leftrightarrow set(y) \wedge \varphi))$$ is an axiom.

Define: $$x=\{y|\varphi\} \iff \forall y (y \in x \iff set(y) \wedge \varphi )$$

Pairing: $$\forall a,b [set(a) \wedge set(b) \to set(\{a,b\})]$$

Define purely accessible ordinal as any ordinal that does not have a subclass of it that is an uncountable regular [weak] limit cardinal; i.e., no inaccessible cardinal is a subclass of it.

Now if we add an axiom stating that any class is a set if and only if it is hereditarily subnumerous to a purely accessible ordinal. Formally this is:

Accessibility: $$\forall x [set(x) \leftrightarrow \exists \alpha (\alpha \text{ is purely accessible ordinal } \wedge \\ \forall y (y \in TC(x) \lor y=x \to \exists f (f:y \rightarrowtail \alpha)))]$$

Where $$\text TC(x)$$ means the transitive closure of $$x$$ defined in the usual manner as the intersectional class of all transitive super-classes of $$x$$.

Would this theory prove the power set axiom for sets? that is:

$$\forall x (set(x) \to \exists y (y=\{z|z \subseteq x\} \wedge set(y)))$$

Note: its clear that if we drop the requirement of $$y=x$$ in Accessibility axiom, then we can get the power set axiom. But here $$x$$ itself must be also subnumerous to some purely accessible ordinal. Can for example $$P(\aleph_0)$$ be equinumerous to the proper class $$ORD$$ of all set ordinals? We note that this theory is as strong as $$\text{ZFC}$$ as regards proving existence of ordinals, i.e. every ordinal provable to exist in $$\text{ZFC}$$ is also provable to exist here as a set ordinal, also all axioms of $$\text {ZFC}$$ except power and regularity are provable here. But apparently the power set axiom is not provable here? The reason why I say that is because the cardinality of the continuum is not controllable, it is consistent for it to even be of inaccessible cardinality. I can see how to interpret $$\text {ZFC - Power}$$ in this theory, i.e. interpret adding Regularity, but I don't know how to interpret the power set axiom? This theory must be able to do that, i.e. interpret power set axiom, although I think it is not able to prove that axiom. I suspect interpreting power can be done through constructible sets, i.e. through $$L$$, since powers in $$L$$ would be subnumerous to pure accessible ordinals via $$\text{GCH}$$. However I'm not so sure.

Your system indeed couldn't prove even that $$\mathcal{P}(\omega)$$ is a set. Let $$M$$ be a countable transitive of $$\mathsf{ZFC}+\mathsf{GCH}+\mbox{there exists an inaccessible}$$. Let $$\kappa\in M$$ be the first inaccessible in $$M$$. Let $$M[G]$$ be the forcing extension of $$M$$ by $$\kappa$$-many Cohen reals. Note that by the standard facts about Cohen forcing, $$\kappa$$ is the first weakly inaccessible in $$M[G]$$ and $$M[G]\models (\kappa=2^{\aleph_0})$$. Let $$K$$ be the transitive model $$(\mathcal{P}(H\kappa))^{M[G]}$$; we will treat $$K$$ as a model of class theory, e.g. $$K$$-sets will be precisely elements of $$(H\kappa)^{M[G]}$$. Clearly, $$K$$ is a model of your theory and in $$K$$ there exists a (class) bijection between the classes $$\mathcal{P}(\omega)$$ and $$On$$ (the latter is due to the fact that in $$M[G]$$ there is a bijection between $$\kappa$$ and $$(\mathcal{P}(\omega))^{M[G]}$$).
However I am not certain whether your theory shows that $$L$$ is an interpretation of $$\mathsf{ZFC}$$. It would be very plausible that it is the case if it would be possible to prove the axiom of collection for sets (naturally formalized as a single sentence in the setting with classes) in your system, but I don't know whether it is indeed possible.
• I think the proof of this Lemma is easy, now if $x$ is bijective to some ordinal $\alpha$ via function $f$, then code each element $m$ of $x$ after that bijection, i.e. by $f(m)$, now let's have a function $r$ that replaces each element $m$ of $x$ by $r(m)$, now $r(m)$ itself is bijective to an ordinal by function $h$, now send each element $m$ of $x$ to the set $\{\langle f(m), h(n) \rangle| n \in r(m)\}$, now the set union of all those sets is clearly well orderable. The rest of proof of replacement (and collection) over sets is simple. May 31 '19 at 21:26