Abstract
In this talk, I will introduce the notion of Gödel doctrine, which is a doctrine categorically embodying both the logical principles of traditional Skolemization and the existence of a prenex normal form presentation for every formula, and I will explain how this notion is related to the Dialectica construction. In particular, building up from Hofstra’s earlier fibrational characterization of de Paiva’s categorical Dialectica construction, I will show that a doctrine is an instance of the Dialectica construction if and only if it is a Gödel doctrine. This result establishes an intrinsic presentation of the Dialectica doctrine, contributing to the understanding of the Dialectica construction itself and its properties from a logical perspective. Finally, I will show how this notion allows to provide a simple presentation and an explanation in terms of universal properties of the rule version of two relevant logical principles involved in the Dialectica interpretation, namely Markov’s principle and Independence of premise.
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.