2

The set $\mathbb R$ is uncountable $-$ a fact I believe is independent of the Axiom of Choice. Even still, only countably many of these elements can be explicitly described. In order to specify the decimal expansion of a real number $0. a_1 a_2 \ldots$ one must give the function $a \colon \mathbb N \to \{ 0,1,2,3,4,5,6,7,8,9\}$ such that $a(n) = a_n$.

But how many of these functions can we hope to describe using, say the standard collection of 26 letters, the digits 0 through 9, and a dozen or so helpful punctuations? Obviously our description must be of finite length. While $0.333 \ldots $ implicitly describes the real number $1/3$ this can be replaced with the finite description '$a(n) = 3$ for every $n \in \mathbb N$'.

A language with only finitely many symbols can only write out countably many algorithms. It follows the set $\mathbb D \subset \mathbb R$ of describables is countable. Let $\mathbb I = \mathbb{R} - \mathbb{D}$ be the set of indescribables. Since $\mathbb R$ is uncountable we can say $\mathbb I$ is non empty.

Note that while '$\mathbb I$ is non empty', no element may be exhibited. No indescribable element can be written down. But acting like no such element exists would result in a logical inconsistency. But without something like the Axiom of Choice there is no way to select a 'generic element'.

But even without the Axiom of Choice we still have '$\mathbb I$ is non empty'. This translates formally to $\exists x \in \mathbb I$ which says not only 'the set is non empty' but also singles out a specific element and calls it $x$. It says 'this one'. While one might ponder the set $\mathbb I$ without any specific element in mind, this pondering does not translate into the standard language of set theory.

Are there any non-standard examples of set theory where can say 'this set is non empty' or 'there exists an element' without also saying 'this one'? has any logical system been studied where the two informal notions correspond to two distinct formal notions?

Further thoughts: If we were intuitionists, would it be sensible to encode the phenomenon above as $\neg \neg (\exists x \in \mathbb I)$, a statement strictly weaker than $(\exists x \in \mathbb I)$?

Andrés E. Caicedo
  • 79,201
Daron
  • 10,300
  • 2
    $\exists x \in \mathbb{I}$ does not assert anything about an object in $\mathbb{I}$ other than that it is in $\mathbb{I}$. $x$ is a dummy variable, so I don't know what you mean by "this". – GFauxPas Apr 12 '15 at 18:36
  • @GFauxPas: Indeed - I'd recommend making that an answer instead of a comment, as it's exactly correct. – Zev Chonoles Apr 12 '15 at 18:42
  • 1
    actually, applying Cantor's theorem to this case is an interesting thing to do because it makes you realize that it's hard to define "describable". – mercio Apr 12 '15 at 19:20
  • If pushed I would define it as saying the function $a(n)$ is computable. Of course then we run into the Church-Turing thesis Beep Bop Boob I am a Turing machine. How does Cantor's theorem come in? – Daron Apr 12 '15 at 19:28

4 Answers4

6

The axiom of choice is not choosing a "generic element". This is a common misconception. The axiom of choice simply asserts that a certain set is not empty.

The actual instantiation of the existential quantifier lies in the actual logic. We know that from $\exists x\varphi(x)$ we can prove that $\varphi(c)$ for a new constant symbol $c$.

And the point here is that when you pick an element from a non-empty set, it really doesn't matter which element it was. If it the choice of element matters, then you need more constraints and those define a smaller collection of elements.

Asaf Karagila
  • 393,674
  • 1
    I would argue the axiom asserts a certain set is non empty BY selecting a generic element. And that these two informal notions are indistinguishable when expressed in the language of set theory. I suppose $\exists x \varphi (x)$ doesn't 'mean anything' until we specify a model. But once a model is specified we take the interpretation of $\exists x \varphi (x)$ as the definition of a certain set being nonempty. – Daron Apr 12 '15 at 18:46
  • 1
    In your second paragraph, you seem to be saying that we have the existence property. Surely you don't mean that. – Zhen Lin Apr 13 '15 at 07:25
  • @ZhenLin: I meant constant symbol, and don't call me Shirley. Thanks. :-) – Asaf Karagila Apr 13 '15 at 08:01
4

You say:

"This translates formally to $\exists x \in \mathbb I$ which says not only 'the set is non empty' but also singles out a specific element and calls it $x$. It says 'this one'."

Not so. $\exists x \in \mathbb{I}$ does not assert anything about an object in $\mathbb{I}$ other than that it is in $\mathbb{I}$. Here $x$ is a dummy variable, and there's nothing "this" about it.

GFauxPas
  • 5,047
4

There are logical systems where saying "the set $I$ is non-empty" is weaker than saying $\exists x\,x \in I$. Namely, constructive set theories such as IZF, in which the latter property is called being inhabited.

In this context, the Axiom of Choice can be shown to imply the law of excluded middle, so it would bring us back to the classical context where being nonempty is the same as being inhabited. But I don't think the way AC does this is the way you suggest that it does.

A separate point is that what you are saying about "descriptions" is difficult to formalize. If you pick some particular, limited system of descriptions, then you can diagonalize to define a real number that is not described in the system. If you want to allow any description whatsoever in the language of set theory, then you run into the undefinability of truth and your argument doesn't work.

Trevor Wilson
  • 16,989
  • ...and to answer the question in your latest edit, I believe that "nonempty" is defined as the double negation of "inhabited" in IZF. – Trevor Wilson Apr 13 '15 at 07:14
2

What you are seeing is, in effect, the failure of the existence property, i.e. it is possible to prove $\exists x . \phi (x)$ without being able to exhibit a closed term $a$ for which $\phi (a)$ is true. This is not so surprising when you realise that $\exists x . \phi (x)$ is just an abbreviation for $\lnot (\forall x . \lnot \phi (x))$ in classical logic.

Of course, there's also a language issue – in the language of set theory, there are no closed terms at all, so set theory fails to have the existence property for trivial reasons. The question is more interesting in other settings, e.g. arithmetic and type theory. You may have heard something to the effect that intuitionistic logic has the existence property – but that is not quite a grammatical statement. The existence property is a property of theories, not logics. It is perfectly possible to have a theory in intuitionistic logic that does not have the existence property: for example, take the theory whose only axiom is $\exists x . x = x$, in a language without any constant symbols.

Finally, it is worth pointing out that the assertion that "there is a closed term $a$ for which $\phi (a)$ is true" is not itself a logical statement, in contrast to $\exists x . \phi (x)$. The former is an assertion about the theory (i.e. metatheoretic), whereas the latter is an assertion in the theory. So it is not reasonable to treat both on an equal footing inside a formal system.

Zhen Lin
  • 90,111