This article is rated Start-class on Wikipedia's content assessment scale. It is of interest to the following WikiProjects:

Mathematics Low‑priority This article is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of mathematics on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.MathematicsWikipedia:WikiProject MathematicsTemplate:WikiProject Mathematicsmathematics Low This article has been rated as Low-priority on the project's priority scale.

Section sizes Section size for Constructive set theory (90 sections) Section name Byte count Prose size (words) Header Total Header Total (Top) 981 981 95 95 Introduction 19 23,163 0 2,186 Constructive outlook 2,152 14,817 247 1,517 Metalogic 4,981 4,981 293 293 Anti-classical principles 7,684 7,684 977 977 History and overview 3,767 8,327 345 669 Models 4,560 4,560 324 324 ECST 1,880 116,652 227 12,320 Notation 1,134 7,301 162 782 Language 923 923 122 122 Variables 733 733 92 92 Classes 2,856 2,856 186 186 Extensional equivalence 1,655 1,655 220 220 On the use of intuitionistic logic 4,126 4,126 556 556 Equality 2,492 3,815 240 405 Alternative approaches 1,323 1,323 165 165 Merging sets 3,826 3,826 349 349 Set existence 1,200 2,462 144 287 Successor sets 1,262 1,262 143 143 BCST 597 17,931 86 2,167 Separation 5,207 5,207 564 564 No universal set 3,128 3,128 433 433 Predicativity 3,209 3,209 442 442 Replacement 3,340 3,340 393 393 Hereditarily finite sets 2,450 2,450 249 249 ECST via Strong Infinity 4,930 14,828 195 1,479 Weaker formulations of infinity 2,076 2,076 246 246 Number bounds 1,296 1,296 146 146 Moderate induction in ECST 6,526 6,526 892 892 Functions 18 30,857 0 3,524 General note on programs and functions 7,450 7,450 908 908 Total functional relations 5,784 5,784 819 819 Finitude 2,909 2,909 456 456 Infinitude 3,367 3,367 468 468 Characteristic functions 4,611 4,611 353 353 Witness of apartness 1,729 1,729 97 97 Computable sets 2,534 2,534 148 148 Boundedness criteria 2,455 2,455 275 275 Choice functions 9,937 14,365 196 677 Full Choice implies PEM 2,413 2,413 312 312 Regularity implies PEM 2,015 2,015 169 169 Arithmetic 19 7,980 0 972 Shortcomings of ECST 1,534 1,534 184 184 Arithmetic functions from recursion 1,976 1,976 223 223 Recursion from set theory axioms 4,451 4,451 565 565 Weak set theory variations 35 7,281 0 895 Induction without infinite sets 6,516 6,516 803 803 Intuitionistic KP 730 730 92 92 Stronger subtheories of ZF 33 68,905 0 7,331 Exponentiation 3,927 16,583 491 1,643 Unions and countability 1,833 1,833 243 243 The class of all subsets of a set 7,170 7,170 458 458 Category and type theoretic notions 2,716 2,716 323 323 Metalogic 937 937 128 128 Analysis 1,078 11,372 117 1,128 Topology 855 855 106 106 Cauchy sequences 537 537 54 54 Cauchy reals 1,283 1,283 167 167 Towards the Dedekind reals 1,682 1,682 219 219 Constructive schools 3,619 3,619 178 178 Indecomposability 2,318 2,318 287 287 Non-constructive principles 5,178 8,417 630 1,002 Infinite trees 3,239 3,239 372 372 Induction 18 8,970 0 1,086 Mathematical induction 2,731 2,731 321 321 Set Induction 2,801 2,801 318 318 Metalogic 1,782 1,782 241 241 Relation to ZF 1,638 1,638 206 206 Strong Collection 3,483 3,831 422 457 Metalogic 348 348 35 35 Constructive Zermelo–Fraenkel 40 5,051 0 383 Binary refinement 1,353 1,353 158 158 Subset Collection 809 809 53 53 Fullness 2,849 2,849 172 172 Metalogic of CZF 564 10,431 69 1,135 Unprovable claims 3,070 3,070 371 371 Ordinal analysis 1,386 1,386 163 163 Models 3,029 3,029 303 303 Breaking with ZF 2,382 2,382 229 229 Intuitionistic Zermelo–Fraenkel 2,938 3,952 345 465 Metalogic 1,014 1,014 120 120 Intuitionistic Z 265 265 32 32 Sorted theories 20 3,420 0 242 Constructive set theory 1,970 1,970 60 60 Bishop style set theory 382 382 49 49 Category theories 1,048 1,048 133 133 See also 594 594 0 0 References 28 28 0 0 Further reading 683 683 0 0 External links 693 693 0 0 Total 215,119 215,119 22,174 22,174

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)

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]

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]

This article is very informative, but also extremely long (23,880 words per https://prosesize.toolforge.org/?title=Constructive+set+theory&domain=en.wikipedia.org, while WP:TOOBIG says articles with >15,000 words should almost certainly be divided or trimmed), and in my opinion impossible to understand for readers not already familiar with the subject.

To improve this, for a start, many of the topics discussed are not specific to constructive set theory but apply to constructive mathematics more generally, whether done in constructive set theory, in type theory, in the internal language of an elementary 1-topos with NNO, etc, so these could become separate pages, e.g., "Real numbers in constructive mathematics", etc. I'll start this if I get the time. Jean Abou Samra (talk) 09:14, 7 September 2025 (UTC)[reply]

I agree and I've thought of this.

For starters, the "Subtheories of ZF" section (which is 4/5th of the page) can be made into its own article "Constructive subtheories of ZF". The "Subtheories of ZF" would then basically just hold a link there. Easy win.

And that part actually contains some outlooks on how the strictly non-classical world looks like, and those could be moved back into trailing sections. The balancing of the three angles is a bit of work. (I.e. agnostic vs classical on top vs niche on top. I mean all the talk that either says "and here's what suddenly happens if you adopt LEM" as well as "and here's some stuff that is actually possible to postulate but even breaks LEM".)

There's then mathematical subjects (the ones which are very natively are written down in se theory), and those could/should get its own constructive mathematics article - notably I'm thinking of the topology R^n and, similarly, the measure theory aspects. Basically, what's math actually like if things are small'ish (no powerset) and you take undecidably (as in CS theory) seriously in a material (non-category theory) world. Those are the subjects which can use constructive set theory and then feel notably different than the classical world. Those subjects are what makes the part after 2^N so long. This and the aforementioned article's responsibility of building the agnostic core, but then commenting on the options, makes it long. (E.g. the elaborations of Choice, or on Indecomposability.) One could think of taking all of this out of a standalone "Constructive subtheories of ZF" page.

On the flipside, "topology of R constructively" has been researched, takes some space here, but also has more to it than what would result from a simple translation of what's here. One can factor it out, but it wouldn't necessarily result in a good article just yet. It can be done, and maybe should, but it will probably result in many small articles, such as Indecomposability (intuitionistic logic). (Which is 20 years old and has always in such a "two paragraph state". Don't know if that's good.)

The above (R, topology, measure theory, i.e. normal math stuff) is in-between the early "models of HA" elaborations and "ordinals and big sets" stuff. The latter is actually still only touched upon in the page. At least the constructive indcution/ordinal stuff is, I think, thankfully covered by type theorists. The big constructive sets, on the other hand (or maybe because of the computer folks) is niche. This to me justifies the elaborations what's needed for having a model of HA, what is most helpful in guiding a reader who knows classical set theory into the constructive outlook.

And finally, there's indeed a few parts which got too lengthy, relatively speaking. In particular the elaborative part on full choice - the Discussion section could actually be removed now, since the Diaconescu's article improved. (Even if a bit of information would get lost.) Secondly, set theory without N, which is akin to working with PA, is touched upon in the page, albeit more than what Rathjen and the type theorists cared most for.

One could further get the size down by splitting it into 3 parts. So:

1. One page for "Elementary constructive set theory", which starts with a word on constructivism, takes over the Notation section and then contains everything up to the Exponentiation section (the section on Choice could be a subsection of its final Function section)

2. The "Constructive subtheories of ZF" which early on links to the "Elementary constructive set theory" article, and then speaks of 2^N, CZF, IZF and Kripke set theory. And their metamathematics.

3. Then the aready existing article, which gives the overview (but Notation section moved out), links to the above two, and then also does the last small section on type theories.

Separation in the constructive context is a difficult to get your head around if one comes with a classical mind, and (since less "is a set") some theorems and non-theorems are a matter of how syntax is used.

The above split into 3 parts is an idea - to cut it short. But I also know that it will be inner pain to decide which info goes where, to keep it readable to the non-expert. The current article is far too long, but at least it's all there on the page. 212.186.132.66

PS: I see the top two talk posts with comments from 2006-2008 are extremely outdated and can be cleaned up also (talk) 12:35, 14 September 2025 (UTC)[reply]

I have gone ahead and split the "Subtheories of ZF" section to Constructive subtheories of Zermelo–Fraenkel set theory, although there will still need to be some cleanup for the newly split article. Gramix13 (talk) 23:37, 1 December 2025 (UTC)[reply]

Sounds good.

As noted above, I'd move the Notation section there too, since it's the vocabulary of the ZF subtheory definitions.

If you seek to kick info, the two "Diaconescu" subsections of the Choice section can probably be kicked entirely (just linked to the page that covers it), and likewise the information of the "Constructive schools" one is also not only particular to set theory.

It's a bit of the headache seeking to trim while not kicking out info that otherwise is just in obscure papers rather than Springer textbook. Like with the Reverse mathematics and the ones listed in the Ordinal analysis page, I think people DO go there to know minimal setup proves what, as opposed to look at those as standalone theories of arithmetic or ordinal/cardinal math. These days the choice-of-framework-to-do-math-in discussion seems to have shifted to typed grounds. Constructive set theory is just another reference point. Those who use it seem to look at it as the weak ZF-like set theory of which their sheaf categories are models of, and those who developed it over the previous years are ordinal analysis people who zoom in on computability in set theory. But Wikipedia's proof theory corner also feels split - it appears as a side note of formal logic and its subfield have a bit of representation here, but I see not organizing principle. The field of proof theory arguably remains more technical than stuff you also teach to engineers, and here doesn't have enough pages to move things out to. Constructivism has about a dozen semi-stubs like Indecomposability (intuitionistic logic) or the intuitionism proper pages, where one could move things to. I've occasionally fleshed out pages over the years, but also the theorem capture I think has more action in the computerized projects these days. ~2025-33331-30 (talk) 16:26, 23 December 2025 (UTC)[reply]

So. What happened here is that

• @Gramix13 split the subsection "Subtheories of ZF" into the article Constructive subtheories of Zermelo–Fraenkel set theory and left it here as just a link.
• @Fram draftified the latter page, probably without noticing its origin, on the grounds that it was not understandable as-is.
• @Shhhnotsoloud removed the link to Constructive subtheories of Zermelo–Fraenkel set theory in this article on the grounds that the subsection was, apart from the link, empty.

Taken all together, this resulted in the effective removal of this huge chunk of content from Wikipedia!

As a damage control measure, I've now reverted the article to its status before the split (and I will delete Draft:Constructive subtheories of Zermelo–Fraenkel set theory shortly).

@Gramix13 Thank you for your effort and sorry about this. If you are going to work on a split again, I suggest to make sure to make the new article looks standalone first (although I appreciate it is not easy to work with such a huge amount of content at the same time).

Also, I don't find "Subtheories of ZF" to be a good candidate for splitting out because in my view, it basically contains all of the core content of the article, with the rest being mostly notations, overview, history and commentary. I think it would make sense to have a separate article on each of the main set theories being discussed (at least IZF and CZF, I'm not familiar with the others). Of course this would require a whole lot of rewriting since currently e.g. the exposition of IZF is done assuming the reader already read the previous text about weaker theories, but I think that's part of what's needed to make all this digestible. Jean Abou Samra (talk) 19:19, 26 April 2026 (UTC)[reply]

Here's a second proposition: One makes a page Elementary Constructive Set Theory (a.k.a. ECST) and for now just write a very minimal intro for that new page. From the current page, leave everything up to including History and overview, move over what follows (everything including Notation to including Induction without infinite sets), and then continue the current pages with Exponentiation. The existing subsection ECST would be renamed Infinite sets, as that subsection characterizes ECST over BCST via Strong Infinity.

This results in two pages of about equal size and a sensible cut based on a named set theory. The new page is then an article of the theory ECST, characterized in section 3.4 in Rathjen's book and developed in the bulk of the text. It covers a lot of the more basic, first-order language and arithmetic codable math, except of course it speaks in set theoretic language (emphasis on countability, pigeonhole principle, that stuff, unions and intersections, etc.)

I wouldn't overthink it for now and just cut. It's not like there's high traffic and I think this is a sensible split.

---

One bullet point not in your comma separated list is models of set theory in other frameworks. For your information, I think one reason why splitting it into too many sub-theories is slightly awkward is in how this corpus of mathematical knowledge actually is used today! The guys who initially defined CZF and IZF in the early 70's aren't working anymore. Rathjen and the group who still develops knowledge of it as set theory really are concerned with ordinal analysis in weak frameworks. In terms of quantity, more people who today are interested in that old and new knowledge do computable type theories, natively constructive categories and maybe constructive arithmetic:

"Hey I have this category with a notion of set membership and I validate this and this and this axiom - what does the literature grant me what theorems of ZF do hold for my set model, despite me not having LEM in the logic?"

You can do the subtheory of CZF without Infinity (Jeon, Hanul (2022), "Constructive Ackermann's interpretation") or if instead you remove Function Spaces/Powerset, you're closer second-order arithmetic (in strength towards what we have in Diener, Hannes (2020). "Constructive Reverse Mathematics"). You can look at the theory T that is CZF without strong Collection and T+LEM is still ZF, and Rathjen has names for all of those and tells you what ordinals they prove exists. CZF was cooked up because it's the set theory you can easily squeeze into Martin Löf type theories. IZF has powersets, is even equiconsistent with ZF. People with topoi might care about them for themselves, but because knowing they model them means this and that math holds in their topos.

If you split those into many theories, basically each stronger one proves the mathematical results of the weaker ones, as the whole thing is a development of more and more axioms towards ZF. The only two subsections that jump out of that development is Non-constructive principles and Breaking with ZF.

---

If you don't demand the new page to be a common named set theory, then instead of letting the current page jump from History and overview to Exponentiation, you could also have go from History and overview to Strong Collection and call it Common ZF axioms over a constructive logic. This would leave the current page with the Strong Collection axiom, which is particular to to CZF, and also leave IZF in the current article. ~2026-11980-38 (talk) 12:18, 30 April 2026 (UTC)[reply]

I have now added the page introduction paragraph for an ECST article (in the current article called "ECST") and moved the elementary explainers ("Notation" and "On the use of intuitionistic logic") together, right after. I.e. everything after the first sentences in "Subtheories of ZF" up until excluding "Exponentiation" can be ripped out and turned into an article on the theory ECST, Elementary Constructive Set Theory. ~2026-11980-38 (talk) 14:32, 4 May 2026 (UTC)[reply]