Is there any set theory without something like the Axiom Schema of Separation?

Question

I appreciate any insight to this question, including suggestions for other terms to learn about first. I am self-taught with regards to set theory and not a mathematician, so my question may not be well-formed. Thank you for your patience!

To get to this question I have read numerous Wikipedia articles (set theory, ZFC, ordinal numbers, limit ordinals, etc.), spoken with some grad friends who study math, and read a paper and part of a book by Thomas Jech.

I wanted to know if there exist set theories in use that do not use an Axiom Schema of Separation. My understanding is that in response to Russell's Paradox (itself a critique of Frege) in ZF we have the Axiom Schema of Separation instead of the Axiom Schema of Comprehension (as Jech teaches in Set Theory).

I've been curious about alternative set theories and have found the Wikipedia pages for NBG (Neumann Bernays Godel) and MK (Morse-Kelley). Am I correct in thinking that both of these have something equivalent to the Axiom Schema of Separation?

I am specifically interested in the following notion: is there a set theory in use today that does not rely on the Axiom Schema of Separation to construct its existents*? It seems the power of the Axiom Schema of Separation is to get out of Russell's Paradox by assuming there exists some other set, say $Y$, that one then 'cuts' from in order to construct the set you really wanted to bring into being (say, set of all $x$ with some property).

I'm curious if there are set theories used today that don't do this move, and if so, how do they deal with Russell's Paradox? In short, I'd love a list of alternative strategies that set theories use to create new sets. (Edited after reading Asaf Karagila's kind answer.)

Thank you.

*Existent is a word borrowed from philosophy. It just means "thing that exists." As I understand ZFC, everything in it is a set, so if we were just talking about ZFC instead of "existent" I could have said "set." But, in Morse-Kelley it seems like sets and classes both exist, so I use the term "existent" instead.

Answer 1

Set theory is only useful if you can actually define new sets, if you can specify that certain properties define sets. Because the whole idea behind sets is to have collections of mathematical objects being "first class citizens" of the mathematical universe. In other words, sets are mathematical objects which are themselves collections of mathematical objects.

Naively it was suggested that every property, every collection we can "describe" in a reasonably consistent way, will be a set. But the many paradoxes of naive set theory show us that this is impossible, the most famous one as you point out, is Russell's paradox.

To avoid Russell's paradox we need to limit comprehension, but without some limited form of it, we're quite powerless to define sets, so we can't do much.

1. $\sf ZFC$ and its close relative have a stronger axiom schema (and it allows us to prove strictly more, in a technical sense). Namely the replacement axiom schema, which says that if there is a function, definable with a first-order formula, then the image of a set is another set.

   This of course implies separation. In its second-order relatives, $\sf NBG$ and $\sf KM$, we need to decide what sort of replacement axioms we allow with regard to class variables. This is the key difference between these two cousins.

   So while we allow more power than just separation, we don't quite reach into the obvious paradoxes of naive set theory yet. Simply because for a contradiction to occur here, we need to find a set (which already exists) and a definable function, whose range is not a set.

2. $\sf KP$ (Kripke-Platek) and its close relatives in fact weaken the separation axiom schema only to certain formulas. These theories are much weaker, but they still have interesting uses in recursion theory.

3. $\sf NF$, Quine's New Foundation, a mysterious set theory whose guiding hand comes from type theory. Here we don't require subsets to be defined from pre-existing sets. Instead we require that formulas will have a certain "typed hierarchy" in the variables appearing there (stratified formulas), and this helps to put a leash on the many paradoxes.

   One peculiar example is that $\sf NF$ has a universal set. The set of all sets exists. Here we remove the issue of Russell's paradox by noting that the formula $x\notin x$ is not stratified. So it doesn't need to define a set.

It is important, however, to point out that all the modern set theories we have, at least those that are worth anything, cannot prove their own consistency, and usually we need to explicitly (or sometimes implicitly) assume they are in fact consistent; or assume even stronger theories are consistent. This means that we don't quite avoid Russell's paradox, as much as "we haven't found a contradiction yet". This comes to show that the many paradoxes of naive set theory just tell us that these collections are not necessarily sets.

My view of Russell's paradox, is that it is not at all a paradox. It is a theorem stating the following:

Theorem. If $A$ is a set, and $B=\{x\in A\mid x\notin x\}$ is a set, then $B\notin A$.

Proof. If $B\in A$, then we can ask, is $B\in B$? And then note that $B\in B\leftrightarrow B\notin B$, of course this is a contradiction. Therefore $B\notin A$.

From this we can draw some conclusions, if the set of all sets exists, then $B$ is not a set at all; or if $A$ is a set, and $x\notin x$ can be used to define a subset of $A$, then there is a subset of $A$ which is not an element of $A$.

The conclusion, if so, is that we don't quite avoid Russell's paradox, as much as tacitly assume that everything is fine, and the paradox in fact proves that a certain formulas does not define a set, but rather a proper class.