Abstract
Gödel’s Dialectica interpretation was conceived as a tool to obtain the consistency of Heyting arithmetic in the 40s. In recent years, several proof theoretic transformations, based on Gödel’s Dialectica interpretation, have been used systematically to extract new content from classical proofs, following a suggestion of Kreisel. Thus, the interpretation has found new relevant applications in several areas of mathematics and computer science. Several authors have explained the Dialectica interpretation in categorical terms. In particular, de Paiva introduced the notion of a Dialectica category as an internal version of Gödel’s Dialectica Interpretation in her doctoral work. This was generalised by Hyland and Hofstra, who considered the interpretation in terms of fibrations. In our previous work, we introduced an intrinsic presentation of the Dialectica construction via a generalisation of Hofstra’s work, using the notion of Gödel fibration and its proof-irrelevant version, a Gödel doctrine. The key idea is that Gödel fibrations (and doctrines) can be thought of as fibrations generated by some basic predicates playing the role of quantifier-free predicates. This categorification of quantifier-free predicates is crucial not only to show that our notion of Gödel fibration is equivalent to Hofstra’s Dialectica fibration in the appropriate way, but also to show how Gödel doctrines embody the main logical features of the Dialectica Interpretation. To show that, we derive the soundness of the interpretation of the implication connective, as expounded by Troelstra, in the categorical model. This requires extra logical principles, going beyond intuitionistic logic, namely (suitable versions of) the Markov Principle (MP) and the Independence of Premise (IP) principle, as well as some choice. We show how these principles are satisfied in the categorical setting, establishing a tight correspondence between the logical system and the categorical framework. This tight correspondence should come in handy not only when discussing the traditional applications of Dialectica, but also when dealing with some newer uses of the interpretation, as in modelling games or concurrency theory. Finally, to complete our analysis, we characterise categories obtained as a result of the Hyland, Johnstone and Pitts tripos-to-topos construction when applied to Gödel doctrines.
Davide Trotta
Postdoc
I am a mathematician, and my research is mainly focused on categorical logic and its applications in theoretical computer science.