DSpace Collection:http://hdl.handle.net/2445/1335592019-09-22T10:19:43Z2019-09-22T10:19:43ZWhen the laws of logic meet the logic of lawsdel Castillo Tierz, Jorge delhttp://hdl.handle.net/2445/1337782019-07-11T08:36:31Z2019-05-23T08:28:05ZTitle: When the laws of logic meet the logic of laws
Author: del Castillo Tierz, Jorge del
Abstract: This master thesis presents a brief introduction to type theory, starting at the simplest systems and building up to the Calculus of Inductive Constructions, the formal theory that lies behind some software tools called 'proof assistants'. We will then study a real-life problem based on an actual law (European Regulation 561 for Road Transport) and show that there exist ambiguous situations. Finally, we will use Coq, a proof assistant, to draft the correctness checking proof of our results on the law.
Note: Treballs Finals del Màster de Lògica Pura i Aplicada, Facultat de Filosofia, Universitat de Barcelona, Curs: 2017-2018, Tutor: Joost J. Joosten2019-05-23T08:28:05ZOn a game-theoretic semantics for the Dialectica interpretation of analysisGonzález Bedmar, Mireiahttp://hdl.handle.net/2445/1335602019-05-23T07:37:15Z2019-05-21T10:14:39ZTitle: On a game-theoretic semantics for the Dialectica interpretation of analysis
Author: González Bedmar, Mireia
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. Joosten2019-05-21T10:14:39Z