Document Open Access Logo

The Gödel Fibration

Authors Davide Trotta , Matteo Spadetto, Valeria de Paiva

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2021.87.pdf
  • Filesize: 0.75 MB
  • 16 pages

Document Identifiers

Author Details

Davide Trotta
  • Department of Computer Science, University of Pisa, IT
Matteo Spadetto
  • School of Mathematics, University of Leeds, UK
Valeria de Paiva
  • Topos Institute, Berkeley, CA, USA

Funding

  • Trotta, Davide: the research is supported by the MIUR PRIN 2017FTXR "IT-MaTTerS".
  • Spadetto, Matteo: the research is supported by a School of Mathematics Full-Time EPSRC Doctoral Training Partnership Studentship.
  • de Paiva, Valeria: the author acknowledges support from AFOSR grant FA9550-20-10348.

Cite As Get BibTex

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) https://doi.org/10.4230/LIPIcs.MFCS.2021.87

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Higher order logic
  • Theory of computation → Proof theory
  • Theory of computation → Constructive mathematics
Keywords
  • Dialectica category
  • Gödel fibration
  • Pseudo-monad

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. S. Abramsky and J. Väänänen. From if to bi : A tale of dependence and separation. Synthese, 167, February 2011. Google Scholar
  2. B. Biering. Cartesian closed Dialectica categories. Annals of Pure and Applied Logic, 156(2):290-307, 2008. Google Scholar
  3. B. Biering. Dialectica interpretations - a categorical analysis (PhD Thesis), 2008. Google Scholar
  4. R. Blackwell, G.M. Kelly, and J. Power. Two-dimensional monad theory. J. Pure Appl. Algebra, 59:1-41, 1989. Google Scholar
  5. A. Carboni and E.V. Vitale. Regular and exact completions. Journal of Pure and Applied Algebra, 125(1):79-116, 1998. Google Scholar
  6. D. Dalen. Logic and Structure. Universitext (1979). Springer, 2004. Google Scholar
  7. V. de Paiva. The dialectica categories. Categories in Computer Science and Logic, 92:47-62, 1989. Google Scholar
  8. J. Frey. A fibrational study of realizability toposes (PhD Thesis). PhD thesis, Universite Paris Diderot – Paris 7, 2014. Google Scholar
  9. J.Y. Girard. Linear logic. Theoretical computer science, 50(1):1-101, 1987. Google Scholar
  10. K. Gödel, S. Feferman, et al. Kurt Gödel: Collected Works: Volume II: Publications 1938-1974, volume 2. Oxford University Press, 1986. Google Scholar
  11. P. Hofstra. The dialectica monad and its cousins. Models, logics, and higherdimensional categories: A tribute to the work of Mihály Makkai, 53:107-139, 2011. Google Scholar
  12. J.M.E. Hyland. Proof theory in the abstract. Annals of Pure and Applied Logic, 114(1):43-78, 2002. Troelstra Festschrift. Google Scholar
  13. B. Jacobs. Categorical Logic and Type Theory, volume 141 of Studies in Logic and the foundations of mathematics. North Holland Publishing Company, 1999. Google Scholar
  14. F.W. Lawvere. Adjointness in foundations. Dialectica, 23:281-296, 1969. Google Scholar
  15. F.W. Lawvere. Diagonal arguments and cartesian closed categories. In Category Theory, Homology Theory and their Applications, volume 2, page 134–145. Springer, 1969. Google Scholar
  16. F.W. Lawvere. Equality in hyperdoctrines and comprehension schema as an adjoint functor. In A. Heller, editor, New York Symposium on Application of Categorical Algebra, volume 2, page 1–14. American Mathematical Society, 1970. Google Scholar
  17. S.K. Moss and T. von Glehn. Dialectica models of type theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, pages 739-748, 2018. Google Scholar
  18. P.M. Pédrot. A functional functional interpretation. In CSL-LICS 2014 - Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science, CSL-LICS '14, New York, NY, USA, 2014. Association for Computing Machinery. Google Scholar
  19. P. Pradic and C. Riba. A dialectica-like interpretation of a linear mso on infinite words. In Mikołaj Bojańczyk and Alex Simpson, editors, Foundations of Software Science and Computation Structures, pages 470-487, Cham, 2019. Springer International Publishing. Google Scholar
  20. M. Shulman. The 2-chu-dialectica construction and the polycategory of multivariable adjunctions. Theory and Applications of Categories, 35(4):89-136, 2020. Google Scholar
  21. M. Tanaka. Pseudo-distributive laws and a unified framework for variable binding. PhD thesis, The University of Edinburgh, 2004. Google Scholar
  22. M. Tanaka and J. Power. A unified category-theoretic semantics for binding signatures in substructural logics. Journal of Logic and Computation, 16(1), 2006. Google Scholar
  23. D. Trotta. The existential completion. Theory and Applications of Categories, 35:1576-1607, 2020. Google Scholar
  24. D. Trotta and M.E. Maietti. Generalized existential completions, regular and exact completions. Preprint, 2021. Google Scholar
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact