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.
$\begingroup$
$\endgroup$
3
-
2$\begingroup$ 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. $\endgroup$– Carl MummertJan 1, 2016 at 22:48
-
2$\begingroup$ Con(ZF) → Con(ZF+¬AC) is an arithmetic statement, and every arithmetic statement provable in ZFC is provable in ZF. $\endgroup$– WojowuJan 1, 2016 at 22:52
-
1$\begingroup$ Related: math.stackexchange.com/questions/378030/… $\endgroup$– Carl MummertJan 1, 2016 at 22:53
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
19
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$:
The completeness theorem holds for countable languages without choice. So if $\sf ZFC$ is consistent, it has a model.
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.
answered Jan 1, 2016 at 22:53
-
$\begingroup$ Dont you need dependent choice, even if everything is countable ? $\endgroup$ Jan 1, 2016 at 23:09
-
1$\begingroup$ Why would you? Fix an enumeration, and use recursion over that enumeration! $\endgroup$– Asaf Karagila ♦Jan 1, 2016 at 23:13
-
$\begingroup$ So you take a well ordering of $\mathbb{P}\cap M$. And at every stage chose the smallest element in the next dense set. $\endgroup$ Jan 1, 2016 at 23:15
-
$\begingroup$ 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. $\endgroup$– Asaf Karagila ♦Jan 1, 2016 at 23:16
-
1$\begingroup$ @vhspdfg: It's not an entirely trivial question. Don't feel bad that the answers are short. $\endgroup$– Asaf Karagila ♦Jan 1, 2016 at 23:44
$\begingroup$
$\endgroup$
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.
answered Jan 1, 2016 at 22:50