Disputed

I'm willing to take your word as to Myhill's theories, but it's only equivalent to a one-sorted theory (with additional predicates) if functions are also (equal to) sets, and ℕ is also equal to a set.

Furthermore, in classical set theory, the power set of a set X is equivalent to the set of functions from X to 2. — Arthur Rubin | (talk) 08:04, 7 May 2006 (UTC)[reply]

2^x is not the power set of x. That would be the law of the excluded middle! As for the rest, the "axiom of non-choice" is essentialy the bridge for functions, and the natural numbers can, and I'm sure you knew this, easily be encoded as sets. But yes, I do realise this all needs expansion and citation. -Dan 16:40, 7 May 2006 (UTC)

What is the difference between 2^x and the power set of x in ~~heretical~~ intuitionistic set theory? (And for that matter, what is the difference between "constructive set theory" and intuitionistic set theory?) — Arthur Rubin | (talk) 17:32, 11 May 2006 (UTC)[reply]

Good questions! Brief answers: The range of a characteristic function is "the class of truth values" if you like. Classically, this class would have be a set with exactly two elements (usually {0,1}). In IZF we don't admit that, but we admit this class is a set (therefore the power set exists). In CZF we don't even admit the class is a set. Now I'm not sure how exactly these would up being associated with intuitionism as opposed to constructivism, but one uses "intuitionistic logic" (LEM not assumed) while being impredicative (admits defining new sets in terms of the universe of all sets, e.g. unbounded quantification in separation axiom), while the other is predicative. -Dan 16:55, 17 May 2006 (UTC)

Last revert.

What exactly was wrong with the improvements I introduced? Not sure if that's the right place to ask the question... 24.215.166.41 (talk) 23:46, 23 December 2007 (UTC)[reply]

The initial part may have been an improvement (I'll have to look more closely), but referring to Peter Aczel's CZF as "a successful attempt ..." is clearly biased. — Arthur Rubin | (talk) 23:52, 23 December 2007 (UTC)[reply]

Fine, eliminate "successful attempt" then. The current state of the article needs improvements, I believe. 24.215.166.41 (talk) 23:57, 23 December 2007 (UTC)[reply]

Perhaps we should eliminate CZF entirely. I seem to recall an article deleted as being unsourced.... But, in any case, the body needs sources other than self-published works, especially since there may be disputes between constructive and intuitionist set theoretians as to what connectives mean. — Arthur Rubin | (talk) 00:56, 24 December 2007 (UTC)[reply]

The Troelstra & van Dalen book "Constructivism in Mathematics: An Introduction vol. 2", Page 619 Section 8 contains discussion of CZF that would be an appropriate source. 129.215.149.99 (talk) 15:06, 28 November 2008 (UTC)[reply]

Semantics of constructive set theory

I plan on adding a section on the semantics of constructive set theory soon^TM. It will cover realizability and realizability-with-truth. In particular, this will provide a very rough proof sketch of the disjunction, numerical existence, and church-thesis properties for CZF. I won't include the category theory stuff (I think based on sheafs?) because I'm not actually familiar with it.

Just posting this in case anyone has any comments or objections. TheKing44 (talk) 13:24, 4 June 2024 (UTC)[reply]