An intuitionistic version of Canter'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-Laf's Intuitionistic Type Theory with the universe of the small types.
An intuitionistic version of Cantor's theorem
VALENTINI, SILVIO
1996
Abstract
An intuitionistic version of Canter'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-Laf's Intuitionistic Type Theory with the universe of the small types.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
