[FOM] Applications of the Axiom of Choice

[b.spitters@cs.ru.nl]

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