In this paper we analyze an extension of Martin-Löf's intensional set theory by means of a set contructor P such that the elements of P(S) are the subsets of the set S. Since it seems natural to require some kind of extensionality on the equality among subsets, it turns out that such an extension cannot be constructive. In fact we will prove that this extension is classic, that is "(A ∨ ¬A) true" holds for any proposition A.
Can you add power-sets to Martin-Loef intuitionistic set theory?
MAIETTI, MARIA EMILIA;VALENTINI, SILVIO
1999
Abstract
In this paper we analyze an extension of Martin-Löf's intensional set theory by means of a set contructor P such that the elements of P(S) are the subsets of the set S. Since it seems natural to require some kind of extensionality on the equality among subsets, it turns out that such an extension cannot be constructive. In fact we will prove that this extension is classic, that is "(A ∨ ¬A) true" holds for any proposition A.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
powMLTT.pdf
embargo fino al 31/12/2029
Tipologia:
Published (publisher's version)
Licenza:
Accesso gratuito
Dimensione
735.38 kB
Formato
Adobe PDF
|
735.38 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
