25 September 2012, Logic Tea, Takanori Hida

Abstract

In the setting of classical arithmetic in all finite types with the principle of dependent choices (DC), we investigate the computational content of the axiom of determinacy (AD): All subsets of the Baire space are determined. Our tools for giving computational interpretations in the classical setting are a negative translation and realizability
interpretation for (intutionistic) arithmetic given in [1].

More precisely, we study the computational content of AD as follows: Firstly, we formalize, in classical arithmetic with the axiom of countable choice, the statement of Gale-Stewart's theorem that all open sets are determined, and show that it is provable even in such a weak system. In view of the soundness of this notion of realizability, we find that the negative translation of the statement of Gale-Stewart's theorem is realizable. Hence, we obtain a realizer of the negative translation of AD if we realize the negative translation of the statement that every subset of the Baire space is open (OP). Syntactic continuity of our calculus in fact enables us to give a realizer of the negative translation of OP.

Using the combination of the negative translation with this realizability semantics, we prove the (relative) consistency of classical arithmetic with DC, AD and the negation of the axiom of choice at higher types. This immediately implies that, in classical arithmetic, DC cannot prove the axiom of choice at higher types.

Since the obtained realizer is complicated, it is not easy to gain a clear understanding of its behavior just by observing its reduction. Therefore, we explain its behavior using Coquand's game theoretical semantics.

[1] S. Berardi, M. Bezem and Th. Coquand: On the computational content of the axiom of choice. J. Symbolic Logic vol. 63, no. 2, pp. 600-622, 1998.
[2] T. Hida: A computational interpretation of the axiom of determinacy in arithmetic. Proc. of CSL'12, pp.335-349, 2012.

The Logic Tea homepage can be found at http://www.illc.uva.nl/logic_tea/. For more information, please contact Johannes Marti (johannes.marti at gmail.com), Sebastian Speitel (sebastian.speitel at gmail.com), or Matthijs Westera (M.Westera at uva.nl).