1 Search Results for "Spadetto, Matteo"


Document
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-dev.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}
}
  • Refine by Author
  • 1 Spadetto, Matteo
  • 1 Trotta, Davide
  • 1 de Paiva, Valeria

  • Refine by Classification
  • 1 Theory of computation → Constructive mathematics
  • 1 Theory of computation → Higher order logic
  • 1 Theory of computation → Proof theory

  • Refine by Keyword
  • 1 Dialectica category
  • 1 Gödel fibration
  • 1 Pseudo-monad

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2021

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail