most recent 30 from http://mathoverflow.net 2013-05-20T13:39:01Z http://mathoverflow.net/feeds/question/5329 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/5329/requires-axiom-of-choice-vs-explicitly-constructible Darsh Ranjan 2009-11-13T09:28:57Z 2009-12-22T05:30:27Z

<p>I think I'm a bit confused about the relationship between some concepts in mathematical logic, namely constructions that require the axiom of choice and "explicit" results. </p> <p>For example, let's take the existence of well-orderings on $\mathbb{R}$. As we all know after reading <a href="http://mathoverflow.net/questions/5116/is-the-existence-of-a-well-ordering-on-r-independent-of-zf" rel="nofollow">this answer by Ori Gurel-Gurevich</a>, this is independent of ZF, so it "requires the axiom of choice." However, the proof of the well-ordering theorem that I (and probably others) have seen using the axiom of choice is nonconstructive: it doesn't produce an <i>explicit</i> well-ordering. By an <i>explicit</i> well-ordering, I simply mean a formal predicate $P(x,y)$ with domain $\mathbb{R}\times\mathbb{R}$ (i. e., a subset of the domain defined by an explicit set-theoretic formula) along with a proof (in ZFC, say, or some natural extension) of the formal sentence "$P$ defines a well-ordering." Does there exist such a $P$, and does that answer relate to the independence result mentioned above?</p> <p>More generally, we can consider an existential set-theoretic statement $\exists P: F(P)$ where $F$ is some set-theoretic formula. Looking to the previous example, $F(P)$ could be the formal version of "$P$ defines a well-ordering on $\mathbb{R}$." (We would probably begin by rewording that as something like "for all $z\in P$, $z$ is an ordered pair of real numbers, and for all real numbers $x$ and $y$ with $x\neq y$, $((x,y)\in P \vee (y,x)\in P) \wedge \lnot ((x,y)\in P \wedge (y,x)\in P)$, etc.) On the one hand, such a statement may be a theorem of ZF, or it may be independent of ZF but a theorem of ZFC. On the other hand, we can ask whether there is an explicit set-theoretic formula defining a set $P^*$ and a proof that $F(P^*)$ holds. How are these concepts related: </p> <ul> <li><p>the theoremhood of "$\exists P: F(P)$" in ZF, or its independence from ZF and theoremhood in ZFC;</p></li> <li><p>the existence of an explicit $P^*$ (defined by a formula) with $F(P^*)$ being provable. </p></li> </ul> <p>Are they related at all? </p>

http://mathoverflow.net/questions/5329/requires-axiom-of-choice-vs-explicitly-constructible/5356#5356 Gerald Edgar 2009-11-13T14:44:49Z 2009-11-13T14:44:49Z

<p>In Goedel's proof of consistency of AC, we in fact get much more. There is an explicit relation defined, which is (provably in ZF) a well-ordering of a certain subset of the reals. It is consistent (and follows from the axiom V=L) that the subset is all of the reals.</p>

http://mathoverflow.net/questions/5329/requires-axiom-of-choice-vs-explicitly-constructible/9532#9532 Ashutosh 2009-12-22T05:30:27Z 2009-12-22T05:30:27Z

<p>Levy has a few interesting things to say on the definability of a set whose existence requires the axiom of choice, see pages 171- 175 Basic Set Theory, Perspectives in Mathematical Logic. In particular, he mentions Feferman's result on the unprovability in ZFC of the existence of definable well ordering of reals.</p> <p>On your last question: Levy mentions an example (exceedingly trivial) of a formula F(x) for which one does have a definable set satisfying it in ZFC although the existential formula "for some x, F(x)" is unprovable in ZF.</p>