Implementing Cantor's Paradise

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 formulae allowed in Cantor's naive 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 contra-dictione quodlibet principles fail. We discuss Fitch-Prawitz Set Theory (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 FP. We establish an intriguing connection between an extension of FP and the Theory of Hyperuniverses: the bisimilarity quotient of the coalgebra of closed terms of FP satisfies the Comprehension Principle for Hyperuniverses.
Type de document :
Communication dans un congrès
14th Asian Symposium on Programming Languages and Systems, Nov 2016, Hanoi, Vietnam. Springer Verlag, 2016, Lecture Notes in Computer Science
Liste complète des métadonnées

Littérature citée [14 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01362819
Contributeur : Luigi Liquori <>
Soumis le : vendredi 9 septembre 2016 - 11:27:49
Dernière modification le : samedi 27 janvier 2018 - 01:31:38
Document(s) archivé(s) le : samedi 10 décembre 2016 - 12:57:25

Fichier

FitchCameraReady.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01362819, version 1

Collections

Citation

Furio Honsell, Marina Lenisa, Luigi Liquori, Ivan Scagnetto. Implementing Cantor's Paradise. 14th Asian Symposium on Programming Languages and Systems, Nov 2016, Hanoi, Vietnam. Springer Verlag, 2016, Lecture Notes in Computer Science. 〈hal-01362819〉

Partager

Métriques

Consultations de la notice

155

Téléchargements de fichiers

160