# “Requires axiom of choice” vs. “explicitly constructible”

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.

For example, let's take the existence of well-orderings on $\mathbb{R}$. As we all know after reading this answer by Ori Gurel-Gurevich, 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 explicit well-ordering. By an explicit 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?

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:

• the theoremhood of "$\exists P: F(P)$" in ZF, or its independence from ZF and theoremhood in ZFC;

• the existence of an explicit $P^\*$ (defined by a formula) with $F(P^*)$ being provable.

Are they related at all?

• I think I'm a bit confused about what you mean by "explicit". Can you clarify whether, for you, the statement "there exists x such that blah" and the statement "there exists an explicit x such that blah" mean the same thing or different things? I think that for you these are different concepts but I'm struggling to formalise the difference. – Kevin Buzzard Nov 13 '09 at 9:39
• Here's a related question. I once saw as an UG a proof that the set of positive reals x such that sin(x)=0 contained a smallest element, and I then saw a definition of pi: it was the smallest x>0 such that sin(x)=0. Is that an "inexplicit" definition of pi? If I instead define pi to be the limit of an infinite series, and then invoke some abstract epsilon-delta theorem that says that infinite series for which the terms decrease rapidly have a unique sum in R, is that then an "explicit" definition of pi? Can someone better versed in logic than me explain the logical point behind the difference? – Kevin Buzzard Nov 13 '09 at 9:47
• In my example, "there exists a well-ordering on $\mathbb{R}$" is a statement (indeed, theorem) of ZFC. On the other hand, "there exists an explicit well-ordering" is not a statement of ZFC: it's a statement about ZFC, that there is a formula of ZFC defining a set that is provably a well-ordering. – Darsh Ranjan Nov 13 '09 at 9:51
• @buzzard, regarding your second comment - those are both explicit definitions, since you can prove that they define unique objects. – Darsh Ranjan Nov 13 '09 at 9:54
• One way to make Darsh's question precise would be to ask whether there is a relation on R given by a formula in the language of set theory, which can be shown to be a well defined order without using choice, and which is a well-ordering in the presence of choice. – David E Speyer Nov 13 '09 at 12:07