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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11577/136996
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 1
  • OpenAlex ND
social impact