2026-07-21T19:38:21Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:14527 2024-03-06T10:54:14Z ddc:004 open_access

The Gödel Fibration Trotta, Davide Spadetto, Matteo de Paiva, Valeria Dialectica category Gödel fibration Pseudo-monad 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. 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Davide Trotta and Matteo Spadetto and Valeria de Paiva 2021 Is Part Of LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.MFCS.2021.87 urn:nbn:de:0030-drops-145272 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.87 eng https://creativecommons.org/licenses/by/4.0/legalcode