The Gödel fibration


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).

May 20, 2021 12:00 AM
Category Theory seminars in Cambridge
University of Cambridge