On the computational content of the axiom of choice

Ulrich Berger

(Swansea University)

This talk builds on a paper with the same title by S Berardi, M Bezem and T Coquand (Proceedings of TLCA'95, LNCS 902, 602-622, 1995). The following story tries to illustrate the problem.

Harry Potter's first Coursework at Hogwarts

The coursework is to get a jewel out of the schools treasure. Since Harry did not pay much attention to the lessons he does not know how to do this by magic, but instead has to use other information he collected when snooping around at Hogwarts. Harry found out that there is an infinite number of secret doors at Hogwarts, and that the Professors McGonagal, Dumbledore and Snape are able to do the following actions:

* If Professor McGonagal is given one after the other a key k1 for the first door, a key k2 for the second door, and so on, she will, after having received a finite number of keys k1, ..., kn, return a jewel. The number n may depend on the keys she got (there are many different keys for each door).

* If Professor Dumbledore is given a number n and a method that produces from any key for the n-th door a jewel, then he will return a jewel.

* If Professor Snape is given a jewel, then he will return for any number n a key for the n-th door.

How can Harry manage to get a jewel with the help of the three Professors?

Hint: use the magic of recursion and continuous higher-order operations.

The puzzle above contains the essence in the problem of finding computational content for the Classical Axiom of Choice. In the talk I will present a solution to this problem and discuss its possible impact to program synthesis from classical proofs.
Thursday 8th March 2001, 14:00
Robert Recorde Room
Department of Computer Science