17
$\begingroup$

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?

Improve this question
$\endgroup$
24
  • 3
    $\begingroup$ 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. $\endgroup$
    – Asaf Karagila ♦
    Commented Jul 10, 2017 at 19:30
  • 1
    $\begingroup$ 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? $\endgroup$
    – Burak
    Commented Jul 10, 2017 at 20:25
  • 1
    $\begingroup$ @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. $\endgroup$
    – Goldstern
    Commented Jul 10, 2017 at 20:38
  • 16
    $\begingroup$ 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. $\endgroup$
    – Andreas Blass
    Commented Jul 10, 2017 at 22:00
  • 2
    $\begingroup$ 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"? $\endgroup$
    – bof
    Commented Jul 10, 2017 at 22:41

1 Answer 1

Reset to default
17
$\begingroup$

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.

Improve this answer
$\endgroup$
6
  • $\begingroup$ 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))$. $\endgroup$
    – Joel David Hamkins
    Commented Jul 10, 2017 at 20:56
  • $\begingroup$ 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.] $\endgroup$
    – Pace Nielsen
    Commented Jul 11, 2017 at 4:10
  • 1
    $\begingroup$ 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. $\endgroup$
    – Joel David Hamkins
    Commented Jul 11, 2017 at 11:34
  • 1
    $\begingroup$ How would you make the notion of uniformity mathematically precise? $\endgroup$
    – Andrej Bauer
    Commented Jul 11, 2017 at 23:04
  • 1
    $\begingroup$ 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). $\endgroup$
    – Joel David Hamkins
    Commented Jul 11, 2017 at 23:20

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .