Abstract
We introduce the notion of a Gödel fibration, which is a fibration categorically embodying both the logical principles of traditional Skolemization (we can exchange the order of quantifiers paying the price of a functional) and the existence of a prenex normal form presentation for every logical formula.Building up from Hofstra’s earlier fibrational characterization of de Paiva’s categorical Dialectica construction, we show that a fibration is an instance of the Dialectica construction if and only if it is a Gödel fibration. his 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.
Davide Trotta
Postdoc
I am a mathematician, and my research is mainly focused on categorical logic and its applications in theoretical computer science.