Abstract
Gödel’s Dialectica interpretation was designed to obtain the consistency of Peano arithmetic via a proof of consistency of Heyting arithmetic and double negation. In recent years, proof heoretic transformations (so-called proof interpretations) based on Gödel’s Dialectica interpretation have been used systematically to extract new content from proofs and so the interpretation has found elevant applications in several areas of mathematics and computer science. Following our previous work on “Gödel’s fibrations”, we present a (hyper)doctrine characterisation of the Dialectica which corresponds exactly to the logical description of the interpretation. To show that, we derive the soundness of the interpretation of the implication connective, as expounded on by Spector and Troelstra, in the categorical model. This requires extra logical principles, going beyond intuitionistic logic, namely Markov Principle (MP) and the Independence of Premise (IP) principle, as well as some choice.We make sure that this tight correspondence extends to the use of the principles above, instead of the weaker rules we had proved earlier on. This tight correspondence should come handy not only when discussing the traditional applications of the Dialectica but also when dealing with newer uses in modelling games or concurrency theory.
Davide Trotta
Postdoc
I am a mathematician, and my research is mainly focused on categorical logic and its applications in theoretical computer science.