DROPS

Document

DOI: 10.4230/LIPIcs.MFCS.2021.87

The Gödel Fibration

Authors: Davide Trotta, Matteo Spadetto, and Valeria de Paiva

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

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

Cite as

Davide Trotta, Matteo Spadetto, and Valeria de Paiva. The Gödel Fibration. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 87:1-87:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{trotta_et_al:LIPIcs.MFCS.2021.87,
  author =	{Trotta, Davide and Spadetto, Matteo and de Paiva, Valeria},
  title =	{{The G\"{o}del Fibration}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{87:1--87:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.87},
  URN =		{urn:nbn:de:0030-drops-145272},
  doi =		{10.4230/LIPIcs.MFCS.2021.87},
  annote =	{Keywords: Dialectica category, G\"{o}del fibration, Pseudo-monad}
}

Search Results

Documents authored by Spadetto, Matteo

The Gödel Fibration

Abstract

Cite as

Thanks for your feedback!

Could not send message