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 formula 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 (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.

Implementing cantor’s paradise

HONSELL, Furio;LENISA, Marina;SCAGNETTO, Ivan
2016

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 formula 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 (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.
9783319479576
9783319479576
File in questo prodotto:
File Dimensione Formato  
FitchCameraReady.pdf

non disponibili

Descrizione: Articolo principale
Tipologia: Documento in Pre-print
Licenza: Non pubblico
Dimensione 501.85 kB
Formato Adobe PDF
501.85 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
aplas16.pdf

accesso aperto

Tipologia: Documento in Pre-print
Licenza: Creative commons
Dimensione 463.77 kB
Formato Adobe PDF
463.77 kB Adobe PDF Visualizza/Apri
honsell2016.pdf

non disponibili

Tipologia: Versione Editoriale (PDF)
Licenza: Non pubblico
Dimensione 415.98 kB
Formato Adobe PDF
415.98 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11390/1091787
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 6
  • ???jsp.display-item.citation.isi??? ND
social impact