Dialectica logical principles via free categorical constructions

Abstract

In 1958 Gödel introduced the Dialectica interpretation [4] to prove the (relative) consistency of intuitionistic arithmetic and, over the years, this in- terpretation has been generalized from a categorical perspective by several authors, leading up to the notion of Dialectica category [2] (or more gener- ally fibration [5]). The most important clause of the Dialectica interpretation is the defini- tion of the translation of the implication connective. It is well-explained in [1, 3] that the crucial point is that this translation validates two logical prin- ciples which are usually not acceptable from a constructive point of view, namely a variant of the principle of independence of premises (IP) and a variant of Markov’s principle (MP). The main purpose of this talk is to provide a categorical explanation of the validity of (IP) and (MP) in the Dialectica interpretation by using the language of Lawvere’s doctrines. To achieve our purpose we employ the tool of existential (and univer- sal) completion introduced in [7] and further developed in [6] to define a proof-irrelevant categorification of the Dialectica interpretation given in [8] in terms of doctrines that we call Gödel doctrines. Then, we show that the categorical notions of existential-free elements introduced in [6] and universal-free elements developed in [8] provide a cat- egorical presentation of quantifier-free formulas and are the key ingredient to validate (IP) and (MP) underlying Gödel’s Dialectica interpretation. Finally, showing that every Gödel doctrine validates also the so-called principle of Skolemization, we can conclude the proof that the notion of Gödel doctrine provides a complete categorical account of the Dialectica interpretation and of the logical principles there involved.
References
[1] Avigad, J. and Feferman, S. (1970). Gödel’s functional (”dialectica”) interpretation. Handbook of Proof Theory, 137.1 \

[2] de Paiva, V. (1989). The dialectica categories. Categories in Computer Science and Logic, 92:47–62.
[3] Gödel, K., Feferman, S., et al. (1986). Kurt Gödel: Collected Works: Volume II: Publications 1938-1974, volume 2. Oxford University Press.
[4] Gödel, K. (1958). Über eine bisher noch nicht benÜtzte erweiterung des finiten stand- punktes. Dialectica, 12(3-4):280–287.
[5] Hofstra, P. (2011). The dialectica monad and its cousins. Models, logics, and high- erdimensional categories: A tribute to the work of Mihály Makkai, 53:107–139.
[6] Maietti, M. and Trotta, D. (2021). Generalized existential completions, regular and exact completions. Preprint.
[7] Trotta, D. (2020). The existential completion. Theory and Applications of Categories, 35:1576–1607.
[8] Trotta, D., Spadetto, M., and de Paiva, V. (2021). The Gödel Fibration. In Bonchi, F. and Puglisi, S. J., editors, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021), volume 202 of Leibniz International Proceedings in Informatics (LIPIcs), pages 87:1–87:16, Dagstuhl, Germany. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.

Davide Trotta

Assistant professor (RTDA)

I am a mathematician, and my research is mainly focused on categorical logic and its applications in theoretical computer science.