How hard is it to show $\mathsf{ZF-Pow}\not\vdash\mathsf{AC}$?

Question

This is motivated by comments on this question.

Let $T_0=\mathsf{ZF-Pow}$ and $T_1=\mathsf{ZF-Pow+\neg AC}$. (Note that there is some subtlety about what precisely $\mathsf{ZF-Pow}$ is; here, I adopt the convention which I believe is now standard that collection is used instead of replacement.)

In one sense it's easy to show that $T_1$ is consistent: since per Cohen we have $\mathsf{ZF}\not\vdash\mathsf{AC}$, a fortiori we cannot have $\mathsf{ZF-Pow}\vdash\mathsf{AC}$. However, this argument uses the assumption that $\mathsf{ZF}$ is consistent (what Cohen actually proved, in an appropriately weak base theory, was $\mathsf{Con(ZF)}\rightarrow\mathsf{Con(ZF+\neg AC)}$). Based on how such questions usually pan out I would argue that we should expect this to be massive overkill:

Can we prove in $\mathsf{PA}$ (or at absolute worst in $T_0$), that $\mathsf{Con(T_0)}\leftrightarrow\mathsf{Con(T_1)}$?

The issue is that forcing/symmetric extensions do not seem to be as useful in this context. For a concrete obstacle, let $\alpha$ be the second smallest ordinal such that $L_\alpha\models T_0$. Then (unless I'm missing something) $L_\alpha$ satisfies "There is a transitive model of $T_0$ but there is no transitive model of $T_1$," the key trick being local countability, so any proof of $\mathsf{Con(T_1)}$ from non-overkill assumptions must rely on nonstandard models.

Answer 1

Work over $\mathsf{ZF^-}$, Zermelo-Frankel set theory without choice and with Collection. I will argue that $\mathsf{ZF^-}$ can interpret $\mathsf{ZF^-}$ with there is a non-well-orderable set of reals, by syntactically formulating the typical construction of the basic Cohen model over $\mathsf{ZF^-}$. The focal point of the argument I will provide is that inductive definitions still work without Powerset.

It should be better to clarify that the above argument can be purely syntactical, as we can treat forcing relations purely syntactic manner. Thus the argument given below shows $\mathsf{PRA}$ proves $\mathsf{Con}(T_0)$ proves $\mathsf{Con}(T_1)$, by the same idea that the usual forcing argument can be deemed as a proof of $\mathsf{Con(ZFC)\to Con(ZFC+\lnot CH)}$ over $\mathsf{PRA}$.

We can see that the forcing relation is still definable from the remaining axioms of $\mathsf{ZF^-}$. The key fact is that using the inductive definition (introduced in Barwise's textbook) instead of constructing a hierarchy using Powerset.

Also, $\mathsf{ZF^-}$ proves the set of all partial functions from $\omega$ to $\omega$ is a set, so Cohen forcing $\mathbb{P}=\operatorname{Col}(\omega\times\omega,2)$ exists. We will see that $\mathsf{ZF}^-$ can define the Basic Cohen model.

For any permutation $\pi$ over $\omega$, we can extend it as a permutation over $\mathbb{P}$ as

• $\operatorname{dom}(\pi(p))=\{(\pi(n),m)\mid (n,m)\in\operatorname{dom} p\}$, and
• $\pi(p)(\pi(n),m)=p(n,m)$.

Let $G$ be the class of all $\pi$ over $\mathbb{P}$. We can extend $\pi$ to a map from $\mathbb{P}$-names to $\mathbb{P}$-names, recursively by $$\pi(\dot{x}) = \{(\pi(p),\pi(\dot{y})) \mid (p,\dot{y})\in \dot{x}\}.$$

However, we cannot correctly form the symmetric filter $\mathcal{F}$, so let us go down to earth and handle it concretely.

For a finite subset $e$ of $\omega$, define $$\operatorname{fix}e = \{\pi\in G \mid \forall n\in e (\pi(n)=n)\}.$$ We cannot prove $\operatorname{fix}e$ is a set unless we know $\mathcal{P}(\omega)$ is a set. For each $\mathbb{P}$-name $\dot{x}\in V^\mathbb{P}$, define $$\operatorname{sym}_G(\dot{x})=\{\pi\in G\mid \pi(\dot{x})=\dot{x}\}$$ as we did over $\mathsf{ZF}$. Now let us call a $\mathbb{P}$-name $\dot{x}$ is symmetric if there is a finite subset $e\subseteq \omega$ such that $\operatorname{fix}e\subseteq \operatorname{sym}_G(\dot{x})$. Now we can define the class of all hereditarily symmetric names $\mathsf{HS}$.

Now consider the forcing relation $\Vdash^{\mathsf{HS}}$ obtained by restricting the range of quantifiers to $\mathsf{HS}$. Thus for example, for $\dot{x}\in{\mathsf{HS}}$,

• $p\Vdash^{\mathsf{HS}} \forall y\phi(y, \dot{x})$ if and only if for any for any $\dot{y}\in \mathsf{HS}$, $p\Vdash\phi(\dot{y},\dot{x})$,

and define the remaining part similarly to the syntactic definition of forcing. (Definition 5.7 of Karagila's Iterating Symmetric Extensions is relevant.) Then we can show that the empty condition $\mathsf{HS}$-forces all axioms of $\mathsf{ZF^-}$. Furthermore, we can prove that the name of the generic filter $$\dot{G}=\{(p,\check{p})\mid p\in\mathbb{P}\}$$ is a set, and $\dot{G}\in \mathsf{HS}$. Hence we can internally argue under the $\mathsf{HS}$-forcing relation that (the empty condition forces) $\dot{G}$ produces a set of reals that is not well-orderable by following the typical argument.