On a game-theoretic semantics for the Dialectica interpretation of analysis

Abstract

Gödel's Dialectica interpretation is a tool of practical interest within proof theory. Although it was initially conceived in the realm of Hilbert's program, after Kreisel's fundamental work in the 1950's it has become clear that Dialectica, as well as other popular interpretations, can be used to extract explicit bounds and approximations from classical proofs in analysis. The program that was then started, consisting of using methods of proof theory to analyse and extract new information from classical proofs, is called proof mining.

The first extension of the Dialectica interpretation to analysis was achieved by Spector by means of a principle called bar recursion. Recently, Escardó and Oliva presented a new extension using a principle called "product of selection functions", which provides a game-theoretic semantics to the interpreted theorems of analysis. This eases the task of understanding the constructive content and meaning of classical proofs, instead of only extracting quantitative information from them.

In this thesis we present the Dialectica interpretation and its extensions to analysis, both using bar recursion and the product of selection functions. A whole chapter is thus devoted to exposing the theory of sequential games by Escardó and Oliva.

In their paper "A Constructive Interpretation of Ramsey's Theorem via the Product of Selection Functions", Oliva and Powell gave a constructive proof of the Dialectica interpretation of the Infinite Ramsey Theorem for pairs and two colours using the product of selection functions. This yields an algorithm, which can be understood in game-theoretic terms, computing arbitrarily good approximations to the infinite monochromatic set. In this thesis we revisit this paper, extending all the results for the case of any finite number of colours.