16

I've never had a problem with the axiom of choice, but it has often confused me how many authors find full choice so much different from finite choice. In my head they seem quite similar. We are picking elements in either case--why treat the infinite case as fundamentally different from the finite one? [Note: This is a rhetorical question, which I answer later, to motivate the remainder of the post.]

Their answer was to emphasize that finite choice was provable in ZF, but the full axiom of choice is independent. Okay, so then I'd delve into the proofs of finite choice, and get even more confused. They'd start with the trivial claim that an empty set has a choice function, the empty function. So far so good. Then they'd work by induction, sometimes skipping all the details. My problem was that this was exactly the point where I (and apparently others, see this previous question) got confused. What axiom of set theory allows someone to pick a single element from a single non-empty set?

The answer to this question is probably obvious to most logicians, but it took me a lot of delving to find it. The answer is: It isn't an axiom of set theory that allows this choice. It is the principle of "existential elimination" from first order logic. In other words, singleton choice is a meta-logical assumption. It says that we interpret the sentence $$ \exists x(x\in y) $$ as asserting the ability to pick (non-constructively) an element $x$ inside $y$. [I'm being a bit informal here, but hopefully you get the idea.]

So in my mind that begs the question of why our semantics does not treat the sentence $$ \forall y \exists x (x\in y) $$ as asserting the ability to pick (non-constructively) for each $y$ an element $x_y\in y$. [The subscript here is merely to emphasize that the choice of $x$ depends on $y$.]

Thus my question:

Is there a natural semantics/language where the sentence $\forall y \exists x\ P(x,y)$ is interpreted as the ability to pick for each $y$ some $x_y$ such that $P(x_y,y)$ holds?

It seems like this is somewhat strengthening the usual interpretation of $\forall$, by allowing infinitely many operations (one for each $y$) simultaneously.

Edited to add: Motivated by Goldstern's comment below, an alternate way to frame my question might be: Is ZF+GC (Zermelo-Fraenkel set theory with global choice) a sufficiently strong theory in which the semantics I proposed above is sound?

Pace Nielsen
  • 18,047
  • 4
  • 72
  • 133
  • 3
    It is not a rule of logic which allows us to prove finite choose. It is the combination of the inference rule and the fact that ZF proves induction. See, if you work over a model with non-standard integers, then inference rules can only get you through the standard integers, but not further. But the fact ZF proves induction for the natural numbers (or whatever it perceives as those) allows us to actually prove finite choice. – Asaf Karagila Jul 10 '17 at 19:30
  • Yes, there is a natural semantics/language where the sentence $\forall y\exists x\ P(x,y) $ is interpreted as the ability to CHOOSE for each $y$ some $x=x(y) $ such that $P(x(y),y)$ holds. Namely, set theory with choice, e.g. ZFC. (I write this as a comment and not as an answer, because I assume that you do not consider ZFC natural enough.) – Goldstern Jul 10 '17 at 19:40
  • You need to be a bit less informal. Logic allows such picks from a nonempty set y. If y is empty then you run into a problem. For n from 1 to infinity, consider : throw balls labeled 10n+I for I from 1 through 10 into an infinite urn and a) for sequence 1, draw out the ball with largest label 2) for sequence 2, draw out the ball with smallest label. Now try one more pick after this. How do you know if the last pick is allowed? How can you guarantee that a certain infinite system of choices exist? For some models of ZF, it doesn't. Gerhard "Hopefully You Get This Idea" Paseman, 2017.07.10. – Gerhard Paseman Jul 10 '17 at 19:47
  • You might find enlightenment in considering the multiplicative axiom which is equivalent to the axiom of choice. I'm sure the correct form is on Wikipedia and is something like 'The infinite Cartesian product of nonempty sets is nonempty'. I think early scholars of AC came up with this version just for people with your question. (For the previous comment of mine, I need the words 'nonempty y' in another paragraph as well.) Gerhard "Who Were Very Likely Themselves" Paseman, 2017.07.10. – Gerhard Paseman Jul 10 '17 at 19:59
  • @AsafKaragila I don't disagree with you. If you read my post, I was very careful to say that the ability to "pick a single element from a single non-empty set" was a consequence of the metalogical assumption. You are right that to go further you need induction in ZF which does require some of the axioms of ZF (or a stronger metatheory). – Pace Nielsen Jul 10 '17 at 19:59
  • @Goldstern Are you sure about that? First, since this choice is being made for all sets $y$ simultaneously, I think you need at least the stronger axiom of global choice. Second, this semantics would be applied to more properties than merely $P(x,y)\equiv x\in y$. – Pace Nielsen Jul 10 '17 at 20:02
  • 1
    I don't really understand what the question is after. (This is not a criticism, I literally didn't understand.) Instead of considering the axiom of choice as a principle that allows you to "choose" elements, consider it as a principle that says certain cartesian products of non-empty sets are non-empty. (The choice really happens when you pick an element from this non-empty cartesian product.) Under this interpretation, what exactly is the question after? – Burak Jul 10 '17 at 20:25
  • @Burak The question really isn't about the axiom of choice, per se. My question is whether or not the proposed semantic strengthening of existential elimination appears in the literature, in a natural and nice way; say in ZF+GC for instance. – Pace Nielsen Jul 10 '17 at 20:30
  • 1
    @PaceNielsen: You are right, global choice fits better. Or - more natural, or less natural, depending on your taste - ZF with an additional predicate which gives a global set-like well-order (which may be used in separation and replacement axioms). Or class theories. – Goldstern Jul 10 '17 at 20:38
  • @PaceNielsen: I think our intuition does treat that sentence the way you wish. $\forall y \exists x P(x,y)$ means that there are $x_y$ around in the universe that you can choose for each $y$ such that $P(x_y,y)$ holds. The only problem is that, if you really want to make that choice, then you have to show that the cartesian product (indexed by the class of $y$'s) of those sets containing $x_y$'s is non-empty. I think if you work with set theories including classes and assume global choice, then you get exactly what you want. – Burak Jul 10 '17 at 20:40
  • 15
    I'm pretty sure I've written this on MO before, but it's easier to repeat it than to find it: The axiom of choice is, despite its name, not about our ability to choose things. It's not about us at all. It's exclusively about the existence of certain sets. – Andreas Blass Jul 10 '17 at 22:00
  • 2
    If we want to prove the existence of a choice set for a set ${a,b}$ of two nonempty sets $a$ and $b,$ it's not enough that we can "choose" elements $x_a\in a$ and $x_b\in b;$ we still need an axiom, the axiom of pairing, to get from the chosen elements $x_a$ and $x_b$ to the choice set ${x_a,x_b}.$ Now suppose you have a denumerable set ${a_1,a_2,\dots}$ of nonempty sets $a_i.$ Given that you can "choose" elements $x_i\in a_i,$ then what? Do you have an axiom saying "given any elements $x_1,x_2,\dots$ the set ${x_1,x_2,\dots}$ exists"? – bof Jul 10 '17 at 22:41
  • @bof The axioms of pairing and union should do the trick. First, for each integer $i$ form the ordered pair $<a_i,x_i>$. Then take the union over $i\in \omega$ of these sets. This is a choice function. – Pace Nielsen Jul 11 '17 at 04:03
  • @AndreasBlass I did say "I'm being a bit informal here." That said, I'd like to delve into your statement a bit more. Are you asserting that there is no sound semantics for which the axiom of choice is interpreted as the ability for us to choose things? – Pace Nielsen Jul 11 '17 at 04:06
  • 1
    @PaceNielsen It might be possible to develop a semantics of the sort you describe, but I'm not aware of any such semantics. In fact, I'm not aare of any attempt to develop a semantics that explicitly deals with us and our abilities; the closest thing I've seen is Brouwer's theory of the creative subject. Developing a semantics that explicitly involves our ability to choose things looks like a huge task. – Andreas Blass Jul 11 '17 at 04:11
  • The axiom of union guarantees the existence of the union of any set of sets. I wonder what set you're applying the axiom of union to, to get your choice function. – bof Jul 11 '17 at 04:20
  • Having read the question and comments (and answer) I think that the following paper may be worth a look, of interest, etc: Velleman, D. J. (1993). Constructivism liberalized. The Philosophical Review, 102(1), 59-84. http://www.jstor.org/stable/2185653. – Benjamin Dickman Jul 11 '17 at 04:26
  • @bof Ultimately, I think your question boils down to what one means by "choosing" infinitely often. For example, how do you interpret your own phrase "given any elements $x_1,x_2,\ldots$"? I took that to mean we have access to a function $f:\omega\to V$ such that $f(i)=x_i$. [Otherwise, what does it mean to be given an infinite list?] Now the fact that ${x_1,x_2,\ldots}$ is a set, rather than a class, follows from an axiom of replacement. – Pace Nielsen Jul 11 '17 at 05:15
  • ...continued... To put it another way, instead of talking about "chosing" I'll start using Joel's more expressive terminology of "uniform choosing", which informally speaking means having access to enough information to work with all the choices at once. [Formally speaking, it must mean asserting the existence of some set, which gets back to Andreas' point.] – Pace Nielsen Jul 11 '17 at 05:19
  • @Andreas How about the more modest goal of interpreting our use of the axiom of choice (rather than the statement of the axiom itself) as us exercising the ability to choose? This seems to be how (semantically speaking) many authors (even prominent set theorists) write about the axiom. – Pace Nielsen Jul 11 '17 at 05:28
  • "it has often confused me how many authors find full choice so much different from finite choice." "We are picking elements in either case--why treat the infinite case as fundamentally different from the finite one?" Perhaps you should back up. Do you have a problem with the axiom of infinity (or large cardinal axioms in general)? I think the "opposing position" (if you want to call it that) is that there is (for both socio-historical reasons and philosophical ones) a difference between finite/infinite. Exactly how this is manifested (as in the rest of your post) is a different question. – post.as.a.guest Jul 11 '17 at 14:28
  • 1
    What if you allow one to introduce function symbols in such cases? – Christopher King Jul 20 '17 at 14:58
  • If you're worried about picking an element from a family consisting of one set, then you should check out "The world's simplest axiom of choice", which deals with (in non-classical logic) a family consisting of at most one set... The fact you noticed it comes down to logic is perhaps not coincidental. – David Roberts Oct 25 '17 at 07:50
  • It appears that someone is going through my old posts and downvoting them. If you don't like the question for some reason, please add a comment explaining why. – Pace Nielsen Mar 30 '20 at 21:31

1 Answers1

16

I like this question very much.

I find the difference between the two readings of $\forall x\exists y\ P(x,y)$ to be similar to the issues often brought up by questions of uniformity in mathematical existence assertions. So this may be a good keyword leading to further discussion. For example, the discussion of uniformity in my answer to the question Can a problem be simultaneously NP and undecidable?.

To explain a little, in the context of computability theory, say, in the ordinary mathematical reading of $\forall x\exists y\ P(x,y)$, there is no reason to think that there should be a computable function mapping each $x$ to such a $y$. But if we assert that the existence claim is uniform, then this means something much closer to the semantics about which you inquire, namely, that there should be a computable function allowing us to pass from $x$ to a witness $y$.

In ZFC set theory, the axiom of choice can be interpreted as the assertion that all existence claims of the form $\forall x\in u\exists y\ P(x,y)$ are uniform, so that there is a function $f$ with domain $u$ so that $P(x,f(x))$ for each $y\in u$. In class theories such as KM, the global axiom of choice is the assertion that all assertions of the form $\forall x\exists y\ P(x,y)$ are uniform, so that there is a class function $F$ with $P(x,F(x))$ for all $x$.

Since the issue of the uniformity of existence assertions is often central in many mathematical domains, I propose that this is the answer to your question.

Joel David Hamkins
  • 224,022
  • I swapped $x$ and $y$ from the use in your question, in light of the common mathematical practice to use $x$ for the independent variable and $y$ for the dependent variable. The question here is about the existence of a function $y=f(x)$ for which $P(x,f(x))$. – Joel David Hamkins Jul 10 '17 at 20:56
  • Your post is getting at the heart of what I was asking about. Thank you! As a follow-up question, is your statement "the axiom of choice can be interpreted as the assertion that all existence claims...are uniform" an informal statement of belief, or a technical statement about soundness of a certain semantic. If the second, is there a place where this is proven? [I expect not, as this seems to be quite specialized.] – Pace Nielsen Jul 11 '17 at 04:10
  • 1
    I had just meant that the (global) axiom of choice is the assertion that from the ordinary reading of $\forall x\exists y$ we may deduce the uniform reading, that is, the assertion that there is a function passing from $x$ to such a $y$. I don't have any specific references to suggest, but I have seen this issue discussed in various contexts, and the issue of uniformity of algorithms is quite commonly discussed. – Joel David Hamkins Jul 11 '17 at 11:34
  • 1
    How would you make the notion of uniformity mathematically precise? – Andrej Bauer Jul 11 '17 at 23:04
  • 1
    That there is a function $f:x\mapsto y$ of the relevant kind, and this would depend on the context. In computability theory, one wants the function to be computable; in ZFC set theory, one wants it merely to exist as a set; in GBC, as a class. In constructive mathematics, one wants....(kindly fill in the blank). – Joel David Hamkins Jul 11 '17 at 23:20
  • ... a section of the (onto) map with codomain $u$. (in one version, anyway, @Joel) The particular flavour of non-classical logic will determine what counts as a function automatically. – David Roberts Oct 25 '17 at 07:47