Since it's just one set and not a collection of sets, you don't need some general rule that will give you a well-defined element from each set in your collection.
Am I missing something?
Since it's just one set and not a collection of sets, you don't need some general rule that will give you a well-defined element from each set in your collection.
Am I missing something?
I suppose, if one had a Turing machine with an oracle for the halting problem, it could produce some elements of this set. And then you could ask, what is the shortest program which generates an element of this set. And then if you had multiple shortest programs, you could order them lexicographically. So that's a way you could pick out a single element in principle, even though it is impossible in practice.
Another example would be the set of numbers that are first-order undefinable. (Meaning, numbers for which there does not exist any sentence in first-order logic which is true only for that number). There is no way using first-order logic to pick out a unique element of that set. But I suppose there is some number which is second-order definable but not first-order definable, and hence we could use a sentence of second order logic to uniquely locate a member of the set of first-order undefinable numbers.
As a generalisation – you can define a set such that you can't pick out any individual member of it using certain resources. But it seems like there is always some way to pick out a unique member of such a set using more resources (a higher Turing degree, higher order logic, etc). Can you define a set so you can't pick out an individual member of it no matter how much resources you use? I think the answer to that is "no".
But what does it mean to pick an element infinitely many times? You have to be very careful about your assumptions there, an inductive proof would only prove you can pick an arbitrarily large number of such elements. To say that you can make a set picking one element each from a infinite collection of sets, even countably infinite, is something you cannot prove inductively. It requires another axiom.
And admitting this axiom suddenly paradoxes like Banach-Tarski are possible.
If so, why can't you do that to fully order any set? Just pick an arbitrary element - that's the smallest one. Now take the original set minus that element, and repeat. Bingo, an ordering!
Maybe you can? Maybe it's only infinite sets where this doesn't work?
You could definitely come up with alternative logical systems to first order logic where "just pick an arbitrary element" is not considered a valid proof strategy, but this would be more an exercise in philosophy and logic than in mathematics. There are good practical reasons for mathematicians to like classical first order logic (such as the fact that Godel's completeness theorem applies to it), so it would be hard to convince most mathematicians to switch to any other logical system. Making classical first order logic weaker makes it unpleasant for the purposes of getting things done for not enough benefit (although intuitionists will fight you over this claim), while trying to make it stronger leads to problems where your logical system needs to magically give you access to truths which are uncomputable in order to be complete ("abstract model theory" tries to make this claim precise).
The trouble is that first order logic doesn't have a built-in concept of "infinity", let alone a rule that says it is valid to "just pick an arbitrary infinite sequence", let alone the full strength of the axiom of choice (which applies even to sets so large that their elements can't be listed via a "sequence"). Such a logical rule can only be added in a logical system which can talk about arbitrary sets or infinite sequences in the first place, which goes beyond first-order logic. So rather than having this rule be a rule of pure logic, the workaround is to add it as a mathematical axiom that applies to the (first order) mathematical theory of sets, which is meant to be a practical approximation to the (ungraspable) "true" collection of rules for "higher order logic".