Abstract
Set-theoretic paradoxes have made all-inclusive self-referential Foundational Theories almost a taboo. The few daring attempts in the literature to break this taboo avoid paradoxes by restricting the class of formulæ allowed in Cantor’s naïve Comprehension Principle. A different, more intensional approach was taken by Fitch, reformulated by Prawitz, by restricting, instead, the shape of deductions, namely allowing only normal(izable) deductions. The resulting theory is quite powerful, and consistent by design. However, modus ponens and Scotus ex contradictione quodlibet principles fail. We discuss Fitch-Prawitz Set Theory (\(\mathsf {FP}\)) and implement it in a Logical Framework with so-called locked types, thereby providing a “Computer-assisted Cantor’s Paradise”: an interactive framework that, unlike the familiar Coq and Agda, is closer to the familiar informal way of doing mathematics by delaying and consolidating the required normality tests. We prove a Fixed Point Theorem, whereby all partial recursive functions are definable in \(\mathsf {FP}\). We establish an intriguing connection between an extension of \(\mathsf {FP}\) and the Theory of Hyperuniverses: the bisimilarity quotient of the coalgebra of closed terms of \(\mathsf {FP}\) satisfies the Comprehension Principle for Hyperuniverses.
Dedicated to Marco Forti for his 70th birthday
Aus dem Paradies, das Cantor uns geschaffen hat,
soll uns niemand vertreiben können.
David Hilbert
Work supported by the COST Action IC1201 BETTY “Behavioural Types for Reliable Large-Scale Software Systems” and by the COST Action CA15123 EUTYPES “The European research network on types for programming and verification”.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Alessi, F., Baldan, P., Honsell, F.: A category of compositional domain-models for separable Stone spaces. Theor. Comput. Sci. 2901, 599–635 (2003)
Abramsky, S.: A Cook’s Tour of the Finitary Non-Well-Founded Sets. CoRR, abs/1111.7148 (2011). http://arXiv.org/abs/1111.7148
Capretta, V.: General recursion via coinductive types. Log. Meth. Comput. Sci. 1(2), 1–18 (2005)
Casinghino, C., Sjöberg, V., Weirich, S.: Combining proofs and programs in a dependently typed language. In: POPL 2014, pp. 33–45. ACM (2014)
Development Team: Assistant, The Coq Proof Documentation, system download. http://coq.inria.fr/
Danielsson, N.A., Hughes, J., Jansson, P., Gibbons, J.: Fast and loose reasoning is morally correct. In: POPL 2006, pp. 206–217. ACM (2006)
Forti, M., Hinnion, R.: The consistency problem for positive comprehension principles. J. Symb. Log. 54, 1401–1418 (1989)
Forti, M., Honsell, F.: Models of self-descriptive set theories. In: Colombini, F., Marino, A., Modica, L., Spagnolo, S. (eds.) Partial Differential Equations and the Calculus of Variations. Birkhäuser, Boston (1989). Dedicated to Ennio De Giorgi on his sixtieth birthday
Forti, M., Honsell, F., Lenisa, M.: Processes and hyperuniverses. In: Prívara, I., Rovan, B., Ruzička, P. (eds.) MFCS 1994. LNCS, vol. 841, pp. 352–363. Springer, Heidelberg (1994). doi:10.1007/3-540-58338-6_82
Forti, M., Honsell, F.: A general construction of hyperuniverses. Theor. Comput. Sci. 156(1&2), 203–215 (1996)
Fitch, F.B.: A demonstrably consistent mathematics. J. Symb. Log. 15(1), 17–24 (1950)
Fitch, F.B.: Symbolic Logic - An Introduction. The Ronald Press, New York (1952)
Girard, J.-Y.: Light linear logic. Inf. Comput. 143(2), 175–204 (1998). doi:10.1006/inco.1998.2700
Grishin, V.N.: Predicate and set-theoretic calculi based on logics without contractions. Math. USSR Izv. 18, 41–59 (1982)
Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. ACM (JACM) 40(1), 143–184 (1993). ACM
Honsell, F., Lenisa, M., Liquori, L., Maksimovic, P., Scagnetto, I.: An open logical framework. JLC 26(1), 293–335 (2016). (First pub. in 2013)
Honsell, F., Liquori, L., Maksimovic, P., Scagnetto, I.: A logical framework for modeling external evidence, side conditions, and proof irrelevance using monads. In: LMCS (2016, to appear)
Jacobs, B., Rutten, J.: An introduction to (co)algebras and (co)induction. In: Sangiorgi, D., Rutten, J. (eds.) Advanced Topics in Bisimulation and Coinduction, pp. 38–99. Cambridge University Press, Cambridge (2011)
Pfenning, F., Schürmann, C.: System description: twelf—a meta-logical framework. In: Pfenning, F., Schürmann, C. (eds.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999). doi:10.1007/3-540-48660-7_14
Prawitz, D.: Natural Deduction – A proof-theoretical Study. Dover Publications, New York (2006)
The Twelf Project. http://twelf.org/wiki/Totality_assertion
Wang, Y., Nadathur, G.: Towards extracting explicit proofs from totality checking in twelf. In: LFMTP 2013, pp. 55–66. ACM (2013)
Watkins, K., Cervesato, I., Pfenning, F., Walker, D.: A concurrent logical framework: the propositional fragment. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 355–377. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24849-1_23
Acknowledgments
The authors are grateful to the anonymous referees, and to Oleg Kiselyov, for many useful remarks and intriguing questions.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Honsell, F., Lenisa, M., Liquori, L., Scagnetto, I. (2016). Implementing Cantor’s Paradise. In: Igarashi, A. (eds) Programming Languages and Systems. APLAS 2016. Lecture Notes in Computer Science(), vol 10017. Springer, Cham. https://doi.org/10.1007/978-3-319-47958-3_13
Download citation
DOI: https://doi.org/10.1007/978-3-319-47958-3_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-47957-6
Online ISBN: 978-3-319-47958-3
eBook Packages: Computer ScienceComputer Science (R0)