The Gödel Fibration
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.
Dialectica category
Gödel fibration
Pseudo-monad
Theory of computation~Higher order logic
Theory of computation~Proof theory
Theory of computation~Constructive mathematics
87:1-87:16
Regular Paper
The Gödel fibration
https://arxiv.org/abs/2104.14021
Davide
Trotta
Davide Trotta
Department of Computer Science, University of Pisa, IT
https://orcid.org/0000-0003-4509-594X
the research is supported by the MIUR PRIN 2017FTXR "IT-MaTTerS".
Matteo
Spadetto
Matteo Spadetto
School of Mathematics, University of Leeds, UK
the research is supported by a School of Mathematics Full-Time EPSRC Doctoral Training Partnership Studentship.
Valeria
de Paiva
Valeria de Paiva
Topos Institute, Berkeley, CA, USA
the author acknowledges support from AFOSR grant FA9550-20-10348.
10.4230/LIPIcs.MFCS.2021.87
S. Abramsky and J. Väänänen. From if to bi : A tale of dependence and separation. Synthese, 167, February 2011.
B. Biering. Cartesian closed Dialectica categories. Annals of Pure and Applied Logic, 156(2):290-307, 2008.
B. Biering. Dialectica interpretations - a categorical analysis (PhD Thesis), 2008.
R. Blackwell, G.M. Kelly, and J. Power. Two-dimensional monad theory. J. Pure Appl. Algebra, 59:1-41, 1989.
A. Carboni and E.V. Vitale. Regular and exact completions. Journal of Pure and Applied Algebra, 125(1):79-116, 1998.
D. Dalen. Logic and Structure. Universitext (1979). Springer, 2004.
V. de Paiva. The dialectica categories. Categories in Computer Science and Logic, 92:47-62, 1989.
J. Frey. A fibrational study of realizability toposes (PhD Thesis). PhD thesis, Universite Paris Diderot – Paris 7, 2014.
J.Y. Girard. Linear logic. Theoretical computer science, 50(1):1-101, 1987.
K. Gödel, S. Feferman, et al. Kurt Gödel: Collected Works: Volume II: Publications 1938-1974, volume 2. Oxford University Press, 1986.
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.
J.M.E. Hyland. Proof theory in the abstract. Annals of Pure and Applied Logic, 114(1):43-78, 2002. Troelstra Festschrift.
B. Jacobs. Categorical Logic and Type Theory, volume 141 of Studies in Logic and the foundations of mathematics. North Holland Publishing Company, 1999.
F.W. Lawvere. Adjointness in foundations. Dialectica, 23:281-296, 1969.
F.W. Lawvere. Diagonal arguments and cartesian closed categories. In Category Theory, Homology Theory and their Applications, volume 2, page 134–145. Springer, 1969.
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.
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.
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.
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.
M. Shulman. The 2-chu-dialectica construction and the polycategory of multivariable adjunctions. Theory and Applications of Categories, 35(4):89-136, 2020.
M. Tanaka. Pseudo-distributive laws and a unified framework for variable binding. PhD thesis, The University of Edinburgh, 2004.
M. Tanaka and J. Power. A unified category-theoretic semantics for binding signatures in substructural logics. Journal of Logic and Computation, 16(1), 2006.
D. Trotta. The existential completion. Theory and Applications of Categories, 35:1576-1607, 2020.
D. Trotta and M.E. Maietti. Generalized existential completions, regular and exact completions. Preprint, 2021.
Davide Trotta, Matteo Spadetto, and Valeria de Paiva
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode