# Dependent choice does not imply “the reals are well-ordered”; citation?

As silly as this sounds, I can't find a proof that the axiom of dependent choice (DC) does not imply that the reals are well-orderable. My memory is that this is a fairly early result in the history of independence proofs in set theory. So, my question is twofold. First, the history part:

When/by whom was it first proved that DC does not imply that the reals are well-orderable?

Second, the mathematical part:

How does the proof go?

(To be clear, I am looking for a proof that $ZF+DC+$"the reals are not well-orderable" is consistent relative to $ZFC$; I am not interested in proofs which require assumptions of extra consistency strength. For example, both $AD$ (which implies that the reals are not well-orderable) and $DC$ are consequences in $L(\mathbb{R})$ of large cardinals, so this gives a relative consistency proof from large cardinals - but that's not what I'm looking for.)

-
So, you're not looking for the Solovay model, then? –  Zhen Lin Aug 15 '13 at 19:20
I am not an expert, far from it – but I find this puzzling: Surely, the reals aren't well-ordered (in the standard ordering) no matter what you do? No smallest element and all that. Did you mean to say «the reals can be well-ordered”? –  Harald Hanche-Olsen Aug 15 '13 at 19:21
@ZhenLin: That's quite obvious from the question. –  Asaf Karagila Aug 15 '13 at 19:22
@Harald: that's a good point, although within logic the statements tend to be used interchangeably. I've fixed it to avoid confusion. –  user28111 Aug 15 '13 at 19:25
Note that $\sf AD$ implies that the real numbers cannot be well-ordered. Unlike what you've written. –  Asaf Karagila Aug 15 '13 at 19:30

The first proof is by Solomon Feferman. It was published as an abstract in 1964:

Feferman, S. Independence of the axiom of choice from the axiom of dependent choices, The Journal of Symbolic Logic, vol. 29 (1964) p. 226

As for the original proof, I don't know if it were ever published in full. Going through another paper of Feferman from that year which dealt with forcing, I can tell you that the methods are not pretty and completely unclear to anyone who didn't sit to study the original forcing papers in depth (not just Cohen's, but also the ones that were immediately published after that).

Truss published a generalization of Solovay's argument, as well as Feferman's argument (from the second paper, not the citation in the first part) in which he investigated models of $\sf ZF$.

Truss, J. Models of set theory containing many perfect sets. Ann. Math. Logic 7 (1974), pp. 197–219.

The discussion on the Feferman-type of construction begins after Lemma 2.2, and continues until the end of the second section.

The construction, essentially is adding $\kappa$ many Cohen reals (finite functions from $\kappa\times\omega$) say $x_\alpha$ for $\alpha<\kappa$. Then considering the model generated by the sequences of $\langle x_\alpha\mid\alpha<\beta<\kappa\rangle$.

In terms of symmetric extensions this is the same as taking permutations of $\kappa$, applying them in the obvious way, and considering the ideal of bounded supports for generating filter. Moreover, this symmetric extension contains all the real numbers of the full generic extension, since every Cohen real is forced by a countable subforcing.

-
Excellent! That certainly answers the first question. –  user28111 Aug 15 '13 at 19:44
I'm not sure about the second question. But I tried. –  Asaf Karagila Aug 15 '13 at 20:10
I feel like this is definitely the sort of thing that should be easy to find - do you think, if the second question doesn't get answered here, it would be appropriate for MO? –  user28111 Aug 16 '13 at 19:07
@user28111: What would be easy to find, whether or not the paper itself was published or not? I don't know. In either way, I found a possibly relevant generalization by Truss from a few years later. It is probable that he was going along the original construction (although in a much more readable language, which still doesn't compare to papers from a few years ago). I could add it here, if you want. –  Asaf Karagila Aug 16 '13 at 19:09
Please do. (I mean, it should be easy to find a proof, if not the first proof, that DC doesn't imply $WO(\mathbb{R})$.) –  user28111 Aug 16 '13 at 19:20