>>12426497Consider and the order given by (or if you want) as smallest element and taken to be true if there exists a nonzero such that .
Now for something else, consider as the real line with its standard ordering, a 2-ary predicate
.
This ordering is not what's called a total ordering, since it has no smallest element.
So let's instead consider a new, total orderings
.
Without loss of generality, let be the smallest element, i.e.
holds true for all .
Turns out that it's a metatheoretical result in logic that in the theory where you characterize , no such total ordering could ever be described.
The axiom of choice implies that for every set, there "exists" a total order on that set. Uhhh.
Very roughly, you can think of it as an existence claim of the form
The debate is about what we want it to mean for there to "exist" a function. E.g. a function is an assignment from a value A to a result B, should the existence claim of a function require from you that given A, you can ackshually characterize B or at least how to get to it in principle?
The situation gets tricky in mathematical theories with mere extensional equality (like virtually all set theories), since comparing inputs and outputs itself becomes an intricate task.
