Please use this identifier to cite or link to this item:
Title: On a game-theoretic semantics for the Dialectica interpretation of analysis
Author: González Bedmar, Mireia
Director/Tutor: Joosten, Joost J.
Keywords: Lògica matemàtica
Teoria de la prova
Tesis de màster
Mathematical logic
Proof theory
Masters theses
Issue Date: 2018
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.
Note: Treballs Finals del Màster de Lògica Pura i Aplicada, Facultat de Filosofia, Universitat de Barcelona, Curs: 2017-2018, Tutor: Joost J. Joosten
Appears in Collections:Màster Oficial - Pure and Applied Logic / Lògica Pura i aplicada

Files in This Item:
File Description SizeFormat 
TFM_MireiaGonzalezBedmar.pdf1.08 MBAdobe PDFView/Open

This item is licensed under a Creative Commons License Creative Commons