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

Question

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.

Answer 1

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.

Answer 2

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.