[Math] “Requires axiom of choice” vs. “explicitly constructible”

lo.logicmetamathematics

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?

Best Answer

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.

Related Question