lo.logic - "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}timesmathbb{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 $zin P$, $z$ is an ordered pair of real numbers, and for all real numbers $x$ and $y$ with $xneq 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?