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:
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.
