The Gödel fibration

Abstract

In this talk, I will introduce the notion of Gödel fibration, which is a fibration 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 fibration is an instance of the Dialectica construction if and only if it is a Gödel fibration. This result establishes an intrinsic presentation of the Dialectica fibration, contributing to the understanding of the Dialectica construction itself and of its properties from a logical perspective. (Joint work with Matteo Spadetto and Valeria de Paiva).

Davide Trotta

Postdoc

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