# [FOM] Applications of the Axiom of Choice

b.spitters@cs.ru.nl b.spitters at cs.ru.nl
Thu Dec 6 07:13:42 EST 2007

```Since Robert Black brought up the question of a constructive proof of
Tychonov. I would like to recall that most of the standard applications of AC
(like Tychonov, Hahn-Banach, Krein-Millman, Gelfand, Alaoglu...)
have a constructive versions. There is a general methodology to remove AC and
classical logic from such proofs. As follows:
The axiom of choice is used to construct a point in a certain topological
space. However, in applications of the theorem this point is not needed, but
only the properties of the topological space. One can then study the
topological space as a complete distributive lattice (a locale) forgetting
its points. Once formulated like this there is a non-constructive (!) proof
that on can always obtain a constructive proof (using Barr's theorem). In
practice, this proof can fortunately be constructed explicitly.

An application of AC to the (constructive) localic version of the theorem then
gives the classical theorem instantly, showing that we have arrived at a
genuine generalization of the result.

A fuller version of this story can be found in Mulvey's paper:
http://www.maths.sussex.ac.uk/Staff/CJM/research/pdf/geomchce.pdf
==
On the geometry of choice

This paper examines the way in which the application of the Axiom of
Choice may be avoided by carefully chosen constructive argument of a
geometric nature. Taking the case of the Hahn-Banach theorem as an instance
of this approach, the paper examines the way in which successive intrusions
of the Axiom of Choice in the classical proof may be stripped away to yield a
constructive treatment of the theorem, rephrased within the context of
locales rather than topological space, obtained in joint work with
J.J.C.Vermeulen. The paper is intended to be accessible to a broader audience
within mathematics, particularly those working within non-classical logical
contexts.
==

Bas Spitters
```