Matteo Spadetto

Dialectica completion and Goedel fibrations

The notion of dialectica construction associated to a finitely complete category, an attempt of providing a categorical version of Goedel's dialectica interpretation, was introduced by de Paiva in her PhD thesis and then generalised by Hyland and Biering to an arbitrary fibration. In this talk we introduce the notion of Goedel fibration, which categorically embodies both the logical principles of traditional Skolemization and the existence of a prenex normal form presentation for every formula. A Goedel fibration is defined by a list of categorical properties, essentially saying that it has "enough" existential quantifier free and universal quantifier free predicates. Taking advantage of Hofstra's recent work relating this notion to the ones of existential and universal completion of a given fibration (doctrine), we characterise the instances of the dialectica completion, showing that these are precisely the Goedel fibrations. Secondly, we describe the categorical structures that behave well with respect to this construction, comparing the proof irrelevant setting (doctrines) to the proof relevant one (fibrations). The talk is based on joint work with Davide Trotta (University of Pisa) and Valeria de Paiva (Topos Institute).