|
|
Re: Detecting whether an informal argument uses the axiom of choice
Posted:
Apr 19, 2012 10:42 AM
|
|
Paul <pepstein5@gmail.com> writes:
> So the process of deciding whether an informal argument uses the axiom
> of choice is not clear to me.
It's not a trivial matter to decide whether an informal argument
invokes choice. David Ullrich has already mentioned an example of a
proof where even people who are by no means set theoretically
unsophisticated often have a difficulty spotting the use of choice, that
of the result that a countable union of countable sets is countable. (My
favourite example is related but a shade more subtle: the proof that
omega_1, the first uncountable ordinal, is not the limit of a countable
sequence of countable ordinals.)
Your confusion however is more basic. Others have provided (perfectly
sensible and positively standard) explanations of why "choosing" in such
statements in proof as "Now, choose a real r such that..." don't require
the axiom of choice, but I think it's best to put this matter a bit
differently. It is commonly said that making a finite number of choices
does not require the axiom of choice. This is true as far as it goes,
but somewhat misleading, for the simple reason that no choices whatever
are actually involved here. That is, in a proof involving a step like
such as
So we know that for a there exists a b such that R(a,b). Let now c be
such as b...
any choicing that's going about is merely a stylistic device used to
enliven and make humanly bearable what essentially amounts to nothing
but purely logical reasoning. Indeed, we know that it's possible to
eliminate this sort of "choosing" altogether, and present the reasoning
with no free variables, as a logician would put it. The end result is
horrible, with every line of the proof looking something like:
If for all a there exists a b such that R(a,b) it follows that...
Since for all a there exists a b such that R(a,b) and Q(a,b) it
follows in particular that for all a there exists a b such that
R(a,b).
Formally we find this sort of system e.g. in some text or other by
Quine. The point is not that there would be any point to actually
writing proofs in this horrid format, but rather that any use of free
variables (variables introduced in proofs by such conventional turns of
phrase as "let now x be a y such that...") is merely logical
bookkeeping. There are no actual mathematical construction
involved. It's all just logic chopping.
--
Aatu Koskensilta (aatu.koskensilta@uta.fi)
"Wovon man nicht sprechen kann, darüber muss man schweigen."
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
|
|
