×

Implementing Cantor’s paradise. (English) Zbl 1485.03031

Igarashi, Atsushi (ed.), Programming languages and systems. 14th Asian symposium, APLAS 2016, Hanoi, Vietnam, November 21–23, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10017, 229-250 (2016).
Summary: 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.
For the entire collection see [Zbl 1347.68009].

MSC:

03B40 Combinatory logic and lambda calculus
03B38 Type theory
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Software:

Agda; Twelf; LLFp; Coq
PDFBibTeX XMLCite
Full Text: DOI HAL

References:

[1] Alessi, F., Baldan, P., Honsell, F.: A category of compositional domain-models for separable Stone spaces. Theor. Comput. Sci. 2901, 599–635 (2003) · Zbl 1051.68102 · doi:10.1016/S0304-3975(02)00037-3
[2] Abramsky, S.: A Cook’s Tour of the Finitary Non-Well-Founded Sets. CoRR, abs/1111.7148 (2011). http://arXiv.org/abs/1111.7148
[3] Capretta, V.: General recursion via coinductive types. Log. Meth. Comput. Sci. 1(2), 1–18 (2005) · Zbl 1125.68038 · doi:10.2168/LMCS-1(2:1)2005
[4] Casinghino, C., Sjöberg, V., Weirich, S.: Combining proofs and programs in a dependently typed language. In: POPL 2014, pp. 33–45. ACM (2014) · Zbl 1284.68125 · doi:10.1145/2535838.2535883
[5] Development Team: Assistant, The Coq Proof Documentation, system download. http://coq.inria.fr/
[6] Danielsson, N.A., Hughes, J., Jansson, P., Gibbons, J.: Fast and loose reasoning is morally correct. In: POPL 2006, pp. 206–217. ACM (2006) · Zbl 1370.68042 · doi:10.1145/1111320.1111056
[7] Forti, M., Hinnion, R.: The consistency problem for positive comprehension principles. J. Symb. Log. 54, 1401–1418 (1989) · Zbl 0702.03026 · doi:10.2307/2274822
[8] 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 · Zbl 0709.03030
[9] 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 · doi:10.1007/3-540-58338-6_82
[10] Forti, M., Honsell, F.: A general construction of hyperuniverses. Theor. Comput. Sci. 156(1&2), 203–215 (1996) · Zbl 0871.68131 · doi:10.1016/0304-3975(95)00087-9
[11] Fitch, F.B.: A demonstrably consistent mathematics. J. Symb. Log. 15(1), 17–24 (1950) · Zbl 0039.24501 · doi:10.2307/2268437
[12] Fitch, F.B.: Symbolic Logic - An Introduction. The Ronald Press, New York (1952) · Zbl 0049.00504
[13] Girard, J.-Y.: Light linear logic. Inf. Comput. 143(2), 175–204 (1998). doi: 10.1006/inco.1998.2700 · Zbl 0912.03025 · doi:10.1006/inco.1998.2700
[14] Grishin, V.N.: Predicate and set-theoretic calculi based on logics without contractions. Math. USSR Izv. 18, 41–59 (1982) · Zbl 0478.03009 · doi:10.1070/IM1982v018n01ABEH001382
[15] Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. ACM (JACM) 40(1), 143–184 (1993). ACM · Zbl 0778.03004 · doi:10.1145/138027.138060
[16] Honsell, F., Lenisa, M., Liquori, L., Maksimovic, P., Scagnetto, I.: An open logical framework. JLC 26(1), 293–335 (2016). (First pub. in 2013) · Zbl 1352.68061
[17] 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) · Zbl 1456.03027
[18] 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) · Zbl 1285.68105 · doi:10.1017/CBO9780511792588.003
[19] 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 · doi:10.1007/3-540-48660-7_14
[20] Prawitz, D.: Natural Deduction – A proof-theoretical Study. Dover Publications, New York (2006) · Zbl 0173.00205
[21] The Twelf Project. http://twelf.org/wiki/Totality_assertion
[22] Wang, Y., Nadathur, G.: Towards extracting explicit proofs from totality checking in twelf. In: LFMTP 2013, pp. 55–66. ACM (2013) · doi:10.1145/2503887.2503893
[23] 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 · Zbl 1100.68548 · doi:10.1007/978-3-540-24849-1_23
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.