z-logo
Premium
Can You Add Power‐Sets to Martin‐Lof's Intuitionistic Set Theory?
Author(s) -
Maietti Maria Emilia,
Valentini Silvio
Publication year - 1999
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.19990450410
Subject(s) - extensionality , extension (predicate logic) , mathematics , constructive , power set , proposition , universal set , set (abstract data type) , set theory , discrete mathematics , mathematical economics , algebra over a field , pure mathematics , computer science , epistemology , philosophy , process (computing) , programming language
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 V ⌝ A ) true holds for any proposition A.

This content is not available in your region!

Continue researching here.

Having issues? You can contact us here