>>13710925In math you can write down properties and you can write down objects which may or may not have that property.
E.g. in arithmetic, you can write down the property of a number n to be even
One number which would in Peano arithmetic fulfill this property is e.g. the number 4, which, if we want to be anal about it, there is written as .
The witness that n fulfills P is the number two, i.e. .
Because indeed Peano arithmetic will prove the instance of the proposition
In words, "The number 4 is even because it's twice the number 2."
To recap, you had a property starting with an "there exists" statement,
,
and some terms like four and two (, etc.)
Consider a set theory like ZF and, there, the real numbers R.
You can prove that no well order on R can be defined. I.e. you can't have term < that has the property of being a well-order, on R.
But now e.g. the well-ordering "theorem" (which over ZF is equivalent to choice) is a property saying
"there exists a well-ordering on every ZF set"
So by adopting the axiom of choice, you have the situation where there's a claim about existence, despite you knowing you can't ever "realize it" (like with 4 above)
So by adopting choice, you commit to an "ontology" of your set theory where "there exists" means less than it could. Then the theory proving function existence is just a formality - it doesn't mean that you can find a function with the claimed properties.
It's a bit more dramatic than e.g. the axiom of set theory that says that for every two sets, there _exists_ a pair holding those. E.g. if x and y are sets, we are find with "{x,y}" being that pair.
But if you say there exists a function, some people might argue that then there should exist something like a map that you can actually use.
