# Does ZF $\vdash$ Con(ZF) $\rightarrow$ Con(ZF+$\lnot$AC)?

Certainly ZFC $\vdash$ Con(ZF) $\rightarrow$ Con(ZF+$\lnot$AC), but the usual forcing argument to construct a model of ZF+$\lnot$AC seems to require choice to find a generic filter.

• Actually, I believe PRA proves $\text{Con}(\text{ZF}) \to \text{Con}(\text{ZF} + \lnot \text{AC})$. There are two key points. First, that the forcing arguments can be turned into syntactic arguments, and second, that we don't need an actual generic filter, just one that is generic for a certain collection of dense sets. I believe Kunen discusses this at some length, IIRC. I will let an expert write a proper answer. – Carl Mummert Jan 1 '16 at 22:48
• Con(ZF) → Con(ZF+¬AC) is an arithmetic statement, and every arithmetic statement provable in ZFC is provable in ZF. – Wojowu Jan 1 '16 at 22:52
• – Carl Mummert Jan 1 '16 at 22:53

This has a simple, almost cop-out, solution: absoluteness.

Note that the statement is in fact a first-order statement in the language of arithmetic. And such statement is provable from $\sf ZF$ if and only if it is provable from $\sf ZFC$.

Since you know the latter, you actually know the former.

Although in reality, you can just verify the following in $\sf ZF$:

1. The completeness theorem holds for countable languages without choice. So if $\sf ZFC$ is consistent, it has a model.

2. Forcing and symmetric extensions work without using the axiom of choice.

So if $\sf ZFC$ is consistent, it has a countable model, where forcing works as usual, symmetric extensions work as usual, and therefore if there is a model of $\sf ZF$ there is one where the axiom of choice fails.

It should also be added that the axiom of choice is not really needed in order to find a generic filter over a countable transitive model. The reason is that the model is in fact countable, so the elements from the forcing poset inside the model make a countable set externally. Using this fact, as well the fact that there are only countably many dense set in the model we can define a generic filter recursively without appealing to the axiom of choice.

• Dont you need dependent choice, even if everything is countable ? – Rene Schipperus Jan 1 '16 at 23:09
• Why would you? Fix an enumeration, and use recursion over that enumeration! – Asaf Karagila Jan 1 '16 at 23:13
• So you take a well ordering of $\mathbb{P}\cap M$. And at every stage chose the smallest element in the next dense set. – Rene Schipperus Jan 1 '16 at 23:15
• Yes. Even better, take a well-ordering of $M$, and at each step take the next element in the next dense set, using the same enumeration. – Asaf Karagila Jan 1 '16 at 23:16
• @vhspdfg: It's not an entirely trivial question. Don't feel bad that the answers are short. – Asaf Karagila Jan 1 '16 at 23:44

Even setting aside the question of filters. In ZF you are constructing a forcing language, with truth values in a Boolian algebra, and all the axiom of ZF+$\neg$AC have non zero truth valuations. This suffices for consistence.