Dialectica principles via Gödel doctrines

Godel'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 Godel'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 Godel'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 Godel fibration and its proofirrelevant version, a Godel doctrine. The key idea is that Godel 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 Godel fibration is equivalent to Hofstra's Dialectica fibration in the appropriate way, but also to show how Godel 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 Godel doctrines.(c) 2023 Published by Elsevier B.V.