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?
