An Intuitionistic Version of Cantor's Theorem

Mathematical Logic Quarterly 42 (1):446-448 (1996)
  Copy   BIBTEX

Abstract

An intuitionistic version of Cantor's theorem, which shows that there is no surjective function from the type of the natural numbers N into the type N → N of the functions from N into N, is proved within Martin-Löf's Intuitionistic Type Theory with the universe of the small types

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 98,098

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Analytics

Added to PP
2013-12-01

Downloads
39 (#459,607)

6 months
4 (#1,166,959)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Add more citations

References found in this work

No references found.

Add more references