Implementing Cantor’s paradise in constructive type theory
speaker: Furio Honsell (Università di Udine)abstract: Set-theoretic paradoxes have made comprehensive and self-descriptive Foun- dational Theories a taboo in the 20th Century. Hilbert claimed in 1925 that: “Aus dem Paradies, das Cantor uns geschaffen hat, soll uns niemand vertreiben konnen”, but mathematicians have taken since an informal and naive set-theoretic background theory as their working framework. Few daring attempts to breach the taboo were made e.g by W.V.O.Quine and M.Forti, by restricting the class of formulae allowed in Cantor’s naive Comprehension Principle, and by E. De Giorgi who advocated for a cautious, open-ended, and non-reductionist approach to the Foundations of Mathematics. A different, intensional and proof theoretic approach to avoid the paradoxes was taken by Fitch, later reformulated by Prawitz. The idea is to restrict the shape of deductions allowing only normal (or normalizable) deductions. The resulting theory is consistent by design, but quite expressive even if modus ponens and Scotus’s principle ex contradictione quodlibet fail. We discuss Fitch-Prawitz Set Theory (FP) and implement it in a Logical Frame-work based on Constructive Type Theory, featuring locked types, thereby providing a flexible interactive all-inclusive Mathematical Framework. This is a kind of Computer-assisted Cantor’s Paradise. In particular, we prove a Fixed Point Theorem, whereby one can show that all recursive functions are definable in FP. Finally, we provide an intriguing connection between an extension of FP and the Theory of Hyperuniverses by Forti and Honsell. Namely we show that the strongly extensional quotient, i.e. the bisimilarity quotient, of the coalgebra of closed terms of Fitch-Prawitz Set Theory satisfies the Genaralized Positive Comprehension Principle for Hyperuniverses. This is joint work M.Lenisa, L.Liquori and I.Scagnetto.
timetable:
Tue 20 Sep, 9:00 - 9:55, Palazzo dei Congressi
<< Go back