I want to coin a theory that can speak about big sets like some of those present in NF, but at the same time comprehend over small collections of them as it is the case in ZFC. Is this known to be inconsistent. In particular I have the following system in my mind.

Have all axioms of Zermelo restricted to well founded sets only. Then add:

Schema of Equivalence classes $R \text { is equivalence relation } \to \forall x \exists y (y=\{z| z \ R \ x\})$

for every definable relation symbol $R$ in the language of set theory.

And add:

Schema of Universal Replacement: $\forall x \exists!y \phi(x,y) \land \forall y \exists!x \phi(x,y) \\\to \exists z \forall y (y \in z \leftrightarrow \exists x \phi(x,y))$

And the axiom schema of Replacement from well founded sets, i.e. only replacements of elements of well founded sets by any kind of sets is allowed. Formally this is:

Schema of Small Replacement: $\forall A (A \text { is well founded } \land \forall x \in A \exists! y \phi(x,y) \\\to \exists B \forall y (y \in B \leftrightarrow \exists x \in A \phi(x,y)))$

Is there a clear inconsistency with this theory?

This way we can speak about the set of all Frege's naturals, about any set sized collection of big sets. Also we can speak of sets of equivalence classes, like the set of all Frege numbers, which is the set of all equivalence classes with respect to bijection, so for any equivalence relation R, we can speak of the set of all equivalence classes with respect to relation R.

[After-note] The above question has been answered by Greg Kirmayer to be inconsistent. A possible salvage of this question would be to restrict the schema of equivalence classes to those equivalence relations that are definable after stratified formulas.

  • 1
    $\begingroup$ Will you remove the word EDIT from the top, so that the final version of the post shows only one version of the question, and a version for which you accept Greg Kirmayer's answer? As it stands, the MO chronology on the answer just refers to "yesterday", so I can not tell what version of the question was current when Greg Kirmayer's answer was given, or what version was current when that answer was accepted. $\endgroup$
    – Matt F.
    Sep 16 '19 at 18:26
  • $\begingroup$ @MattF. Done! Thanks. $\endgroup$ Sep 16 '19 at 19:15

The Schema of Equivalence classes is inconsistent with the existence of an empty set. To see this let R be the equivalence relation defined by xRy iff ((x is not in x) and (y is not in y)) or x=y. By the Schema of Equivalence classes {𝑧|𝑧 𝑅 0} exists where 0 is empty.


Church’s Set Theory with a Universal Set, and my variant of it, though not Mitchell’s† can do some of what you ask, e.g. schema of Replacement from well founded sets, but not, I think, the set of all Frege numbers.

† Bibliography at “A Variant of Church’s Set Theory with a Universal Set in which the Singleton Function is a Set” (abridged), in Logique et Analyse, Vol 59, No 233 (2016) pp. 81–131. The full version is available at the Centre National de Recherches de Logique: http://www.logic-center.be/Publications/Bibliotheque/SheridanVariantChurch.pdf.

  • $\begingroup$ well this system also have the singleton function being a set. $\endgroup$ Sep 14 '19 at 12:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.