reason why df-clab, df-cleq and df-clel should be reordered

[wlammen]

df-cleq and df-clel are actually axioms. Here is the detailed reason why. In my eyes df-clab is a definition and should follow both df-cleq and df-clel. Both of these axioms prepare the ground why df-clab is defined as it is. A reason for this will follow. For now propose to mark df-cleq and df-clel as axioms.

[wlammen]

Added my version of df-clab now. Putting it after df-cleq and df-clel renders some of the text in its description pointless

[langgerard]

Thank you very much for this detailed explanation. I have two remarks
1/ Regarding the point 3 of ax-wl-cleq-1, maybe it would be useful to mention that the rules may have more than one wff as input, but only one wff a output;
2/ If the syntax of the ZFC set theory only allows quantification on set variables (so not on class variables), the syntax of other set theories such as NBG or KM allows quantification on class variables. in these theories, a more natural and seemingly more general axiom for class equality would be ax-cl-cleq /- (A = B <--> (A.C (Ce.A <--Q> Ce.B))
In fact, after the introduction of the axiom ax-cl-el (identically ax-wl-eq) /- (Ae.B <--> (E.x (x = A AND xe.B))),
it seems that we have /- (A.C (Ce.A <--> Ce.B)) <--> (A.x (xe.A <-->xe.B)), so that this generalization is not useful.

[wlammen]

1/ From ax-wl-cleq-1, point 3:

Typically, a rule describes an operator (a constant in the grammar)
applied to one or more variables, possibly of different types (though at
this stage we only have "wff").

Ok, "applied to one or more variables" does not use the word "input", which might be more standard, I have no clue. I
borrowed the language from grammar in computer science. In your words: The input need not be wff only, A. x ph uses mixed input, setvar and wff.

Each such rewrite rule is assigned the type "wff".

describes the "output".

2/ A natural question is why not quantify over classes. My home-brewed answer was so far: That would make classes full scale objects not different from sets any more. We aim at establishing proper set theory where proper classes exist as auxiliary constructs only, at best removable from final results.

Nice to learn that there is a theory NBG or KM having a look at quantification over classes. I am afraid my theoretical background does not allow me to elaborate on the consequences more. I often can only work set.mm immanently, I have no time for extensive studies.

That finally leads me to the intention of my PR. In my eyes the current order of theorems df-clab, df-cleq and df-clel is awkward and has lead to questionable comments there. I try to give here a precise description of the role these theorems could have, hopefully useful for discussions . Once this PR is accepted, I will open an issue requesting a reorder, and the publicly available contents of this PR might serve as an input for discussions. Should my request find broad acceptance, I will reorder the block of theorems. In the wake comments need to be adjusted. The version I give here is likely not that of the final result, which should be way more concise.

[jkingdon]

If the syntax of the ZFC set theory only allows quantification on set variables (so not on class variables), the syntax of other set theories such as NBG or KM allows quantification on class variables

While we mention NBG and Morse-Kelly in places like https://us.metamath.org/mpeuni/ru.html and https://us.metamath.org/mpeuni/mmset.html#class , I don't think we need to go beyond that kind of brief mention in set.mm.

[jkingdon]

That finally leads me to the intention of my PR. In my eyes the current order of theorems df-clab, df-cleq and df-clel is awkward and has lead to questionable comments there. I try to give here a precise description of the role these theorems could have, hopefully useful for discussions

I have refrained from commenting so far because I don't think I have a very clear understanding of the issues. I probably don't object to having your perspective in your mathbox, but just sticking something in a mathbox which no one else has read doesn't exactly advance the goal of a discussion.

The version I give here is likely not that of the final result, which should be way more concise.

Totally like the goal of coming up with something concise. One of the things that has made it hard to understand what is really going on with df-clab, df-cleq and df-clel is that I suspect we may have too many words about them (but if we need to remove some words, I don't know which ones!).

[wlammen]

When well-formed formulas are introduced to Metamath at the very beginning, you cannot refer to anything before. You are in a point blank situation.

How is bootstrapping accomplished then? You first pimp up your grammar a bit. This includes adding, in Metamath terms variables of wff type, in grammar terms non-terminal symbols, to it. Then you add, in Metamath terms syntax definitions, in grammar terms rewrite rules, for the most primitive and foundational formulas. In Metamath -> and -. are picked for this purpose; they will never be defined. Axioms are instead used to narrow their semantics down to what you want them to be.

Definition of <-> follows, a bit weird, because the full range of expressiveness is still missing.

Later objects, or classes, are introduced, and again you are in a point blank situation, so how to proceed? Follow the pattern you already developed above! Pimp up the grammar by adding variables for classes. Then add syntax definitions for the most primitive operators e. and =. Use axioms df-cleq and df-clel to narrow their semantics down, so the class versions of ax-7, ax-8, ax-9 and ax-ext hold.

Introduce a formula for class abstractions, still a bit weird, because full expressiveness is missing. In df-clab a form was chosen, that smoothly integrates with the above equality and membership, and allows for elimination, a key feature of definitions.

That's a short summary of what I've written for my mathbox. Of course additionally taking many details like setvar variables into account.

In set.mm definition df-clab is put first instead, This leads to an awkward comment, that has to justify details that later will be expressed by equality and membership anyway. If you think of it as an ordinary definition, it should be added after the axioms, in my view.

[icecream17]

It seems merging this means the community will change df-cleq and df-clel in the future. But there are still questions/conversation, so holding off on approving

[icecream17]

A key paragraph here, great explanation

---

(The other hand was that, the class variable axioms are definitions since class variables are eliminable and the axioms conservative [over the base language])

The following idea/question might give insight:

class x
class { x | ph }
class { x e. A | ph }
class _V
class ...

Above are special cases of class A: cv, cab, crab, cvv etc. Here cab ≈ df-clab is used as the example. Actually, this special case is general for all valid substitutions of the variables in df-clab. df-clab could be considered to cover multiple cases.

Likewise, df-cleq and df-clel cover multiple cases (well, all cases) of class A... except for class x (the hypotheses guarantee that earlier work covers that case). So in a sense, the class variables were partially formed in predicate calculus.

Is this enough? Note that while the concept of classes are still incomplete after predicate calculus, the concept of class abstractions is incomplete until df-clab.

In propositional logic, there was nothing to build off of, a basic new idea was created 'from scratch', so obviously ax-mp to ax-3 are axioms. However ~ cv blurs this line for classes, it is not obvious to me that they are axioms.

Edit: Note that ~ cv counts as material involving -the meaning of- class variables, despite not having class variables A or B or C... At least, describing the special initial cases of -> and -. does not seem obviously different than describing the special case ~ cv

[wlammen]

One can even think of formulas describing a completely new type of a class. It is allowed to have several class builders in parallel, although I cannot think of a useful extra one right now.
cv is one of them, df-clab another.

If one starts with set theory with classes right from the beginning, simplifications are possible. We have to accept, though, that we need the setvar to express ideas outside of set theory, built upon universes with other elements. This compromise has its downsides, especially that you have to consider more cases, and definitions extending others.

Here I am too limited in my knowledge to find the ultimate solution. I just provide a suggestion, that others may further elaborate upon.

[langgerard]

Maybe a concise presentation of the fundamentals of a Theory of Sets and Classes could be like the following.
Our Theory of Classes and Sets works with two types (maybe "type" is not the correct wording ?) of objects :
Classes (written like A, so class A) and Sets (written like x, so class x), with the provision that every set object is also a class object (cv, so that class x).
Moreover, two binary relations are linking pairs of classes (so also pairs of sets, or a class and a set, or a set and a class) :
The relation of equality (written A = B, so weq) and the relation of elementhood (written A e. B, so wel).
Beginning with these two basic primitive relation, the well-formed formulas (wff, written phi) of our theory are recursively built using the unary logical connective of negation (written -., so wn), the binary logical connective of implication
(written -->, so wi) and the universal quantification restricted to set variables (written A.x phi).
Classes, Sets, Equality and Elementhood must obey the following rules :
#1 : Equality of classes "Two classes are equal iff they have exactly the same set elements "
/- (A = B <--> A.x (x e. A <--> x e. B))
#2: Restriction of elementhood " Among classes, only sets can be element of a class "
/- (A e. B <--> E.x (x = A AND x e. B))
#3 : Determination of classes from well-formed formula
" Every wff phi determines a class, noted (x / phi), whose elements are all sets x such that phi(x) is true "
/- ((A = (x / phi)) <--> (y e. A <--> (y/x) phi))
Caution : Two distinct wffs can very well determine the same class.
For example, in the case that the wff psi is the wff (phi AND phi), we have A = (x / phi) = (x / psi).
Moreover, at this moment, it remains possible to have classes that are not determined by some wff.

[wlammen]

Moreover, at this moment, it remains possible to have classes that are not determined by some wff.

Yes, there might be other class builders.

[wlammen]

I don't know what to do to get this acknowledged as my personal perception on how a new concept like wff is added and how the new concept of objects aka classes can be added in close accordance. Adding a disclaimer like "Don't read any further unless you are told so"?

[icecream17]

If my comment above is false:

It seems merging this means the community will change df-cleq and df-clel in the future. But there are still questions/conversation, so holding off on approving

then it counts as an approval. Noting other possibilities can also be done by "there are other interpretations" or such.

[LegionMammal978]

At the point where df-cleq is introduced, the foundations of set theory with classes are being laid. A central property of objects is what elements they contain, expressed by the membership operator e.. Quantification ( A. x ) applies only to objects that a variable of kind setvar can hold. These objects will henceforth be called sets. Some classes may not be sets; these are called proper classes. It remains open at this stage whether membership can involve them.

The formula given in df-cleq (restated below) asserts that two classes are equal if and only if they have exactly the same sets as elements.

Equality, however, is not automatically identical with indistinguishability; this is the case only if equality is indeed the finest-grained relation between classes. Since quantification over classes is not possible, no analogue of ax12v can be formulated. In particular, classes may in principle contain additional elements beyond what set variables can express.

This is the part where I lose the argument. The fundamental conceit of set.mm is that it does not aim to define a "set theory with classes", it aims to defines a set theory with sets, subject to the ZFC axioms. As Norm Megill put it himself back in 2021:

Adding new axioms for class theory sends the message that FOL= + ZFC is not sufficient for mathematics, when in fact all uses of df-cleq and df-clel can be eliminated by converting the notation back to the the native ZFC language (or more accurately to our scheme language, since class variables map to wff variables). It's just not a "direct" substitution of definiens for definiendum like the other definitions in set.mm. No new mathematics results from df-cleq and df-clel; they just provide a convenient notational device that makes set theory much more practical to work with.

In service of this goal, classes in set.mm are not interpreted their own objects with possibly-strange semantics, but simply "wff (meta)variables in disguise". When we write A = B in set.mm, we are not attempting to make any statements about "class objects", nor about their distinguishability: we are only making statements about the formula A. x ( x e. A <-> x e. B ) (for a dummy setvar x), no more and no less.

Of course, the Metamath language doesn't care one whit about how we interpret variables of type class, but the question of axioms vs. definitions is all about our interpretations. Otherwise every new wff construction would be a true axiom, since it similarly adds a new symbol which may inherently have all sorts of strange semantics until we constrain it.

To put it another way, I disagree with the statement that "In practice, however, the more direct and fruitful approach is not to construct class equality from membership, but to treat equality itself as axiomatic." If we wanted set.mm to no longer describe a theory of sets but a theory of class objects, then we would be better served by an actual theory of classes such as NBG, complete with things like classvars. As it stands, there's no real fruit borne by introducing nebulous class objects that cannot be quantified over.

The way I see it, the only real oddity is "If x e. A is a more primitive notion than A = B in set.mm, then why do we write class-syntax definitions as (e.g.) |- _V = { x | x = x } and not |- ( y e. _V <-> y e. { x | x = x } )?" But this is ultimately just a matter of style. Every definition in set.mm has a double meaning: first, it extends the metalanguage with new provable |- statements, and second, it provides a guide for how to eliminate the expression. As far as the first meaning goes, each form can be converted to the other with some unobjectionable FOL axioms.

Meanwhile, the second meaning, of how to eliminate an expression, does not really depend on the metalogical behavior of <-> nor =, as long as we can agree on what rewrite rule it is indicating. When we see the definition |- _V = { x | x = x }, we know that it indicates the rule "in any proof involving _V, replace each instance of _V with { x | x = x } for a fresh setvar x". (Then, once we only have class abstractions left, we can finally apply df-clel, df-cleq, and df-clab to get rid of them.) In the most extreme example, we have df-bi: the rewrite is not at all clear from its lengthy expression, but we can declare by fiat that the rule is "replace each instance of ( ph <-> ps ) with -. ( ( ph -> ps ) -> -. ( ps -> ph ) )". So ultimately, |- _V = { x | x = x } works just as well as |- ( y e. _V <-> y e. { x | x = x } ) as far as eliminability goes.

[LegionMammal978]

Actually, looking at the comments again, another part leaves me scratching my head: you argue that A = B is a more fundamental concept than x e. A, but then leave x e. A as the formula with no inherent definition. In support of this, you point to ceqsal1t as an example of a statement that can be made about class equality without having to use the extensional definition df-cleq. But ceqsal1t doesn't really say anything at all about x = A: since it's meaningless without the definition, we can put any arbitrary wff we want in its place, even on the metalogical level!

  $( A more general version of ~ ceqsal1t , showing that it can't tell us
     anything more about ` x = A ` than any other wff ` ch ` . $)
  ceqsal1t-wff $p |- ( ( F/ x ps /\ A. x ( ch -> ( ph <-> ps ) ) ) ->
      ( ps -> A. x ( ch -> ph ) ) ) $=
    ( wnf wb wi wal biimpr imim2i com23 alimi 19.21t imbitrid imp ) BDEZCABFZGZ
    DHZBCAGZDHGZSBTGZDHPUARUBDRCBAQBAGCABIJKLBTDMNO $.

If you think that A = B can have useful axioms apart from its extensional definition in terms of x e. A, I'd be interested in seeing them. Without those, I don't see any compelling case for separating it from the definition in the same way we separate FOL-with-equality from ZFC, or separate ZFC from the complex-number axioms.

[wlammen]

Thanks for looking into this PR again. I only have limited time to react on it right now, I'll look into it in greater detail later, perhaps during weekend. Still some quick ideas spring to my mind while reading your text.

Yes, NM tried to provide a theory that uses classes only as temporary and artificial expressions, as a convenient shorthand in proofs. For all practical purposes this holds in my view, but I see two loopholes.

1. Most of the combinations x = y, x = A, A = x, A = B, x e. y, x e. A, A e. x, A e. B can be eliminated, with two exemptions
   x e. y and x e. A (well if you have x e. A then x e. y is given as well). They are essentially undefined, and since they are, you not only can assign to them any meaning you like, you can establish a new grammar around them, so they behave in a way unexpected in set theory. For instance, you may think of a class having an extra property like a color (or colors be also classes), that you somehow can access by a notation different from { x | ph }.

Yes, the two class builders cv and df-clab need not be the only class builders, there may be multiple more. This is NOT ruled out, maybe not even stated as a desired outcome somewhere.

This effects A = B (if you want it to be more than an equivalence relation, but express indistinguishability), that now surprisingly may also be dependent on the color of a class. BJ knew of this loophole as he explicitly states in one of his comments around eliminable1, that he considers classes only in the standard form { x | ph }.

2. As a remedy you might now demand that no extra class builder besides cv and df-clab exists. This helps with the color of classes misconception. But it leaves open whether all classes have a sensible notation as { x | ph }. It is suggested by NM to use A = { x | x e. A } here, but that looks fishy to me. If I apply df-clab to x e. { x | x e. A }, I end up with x e. A again, so this is NOT a valuable replacement for an arbitrary class A in my eyes. You might then demand that ph is an expression free of class variables, but, for one, I know no way to formulate this condition in set.mm, and second, I see a murky field around countability. If ph is a usual expression made up of basic notations ->, -., A., = and e. there are only countable many of them. It is known that the real numbers is a set of more than countable sets, so some are NOT expressible in this way.

---

Finally I'd like to point out the goal of my PR here. I don't want to solve all questions around the theory of sets. I want to order three statements as given here: df-cleq, df-clel and df-clab. This reorder leaves the statements intact. It allows for better comments, though, in addition one might turn df-cleq and df-clel into axioms (which they are if x e. A is in principle undefined), but the latter is not mandatory. Since the statements don't change, this reorder does not hinder later modifications discussed elsewhere. And above all: this PR reasons only, based on the current state of affairs. It is in my mathbox, and need not be perfect, or express all the gory details a thorough discussion could uncover.

You took your time to read through my PR, and I will do the same with your comments, once I have more time to spend.

[wlammen]

A quote from @LegionMammal978

... the foundations of set theory with classes are being laid.

I remember I first only used "set theory", and later added "with classes", since df-cleq is about classes, which I wanted to point out.

Is "set theory with classes" a standing term among experts excluding ZF? If so, I am unaware of it, and I apologize for misleading. Maybe "set theory using a notation of classes" would have been more appropriate. Keep in mind, though, the material given in this PR is NOT a scientific paper fit for any kind of scrutiny. Instead I wanted to give detailed reasons for a particular change, that is NOT fundamental. I deliberately took the freedom and used, for example, "set" as a replacement for "set variable viewed as a class by class builder cv", for the sake of brevity, and under the assumption that the gist of it is most often guessed right.

The following citation is from Wikipedia

ZF set theory does not formalize the notion of classes, so each formula with classes must b>e reduced
syntactically to a formula without classes. For example, one can reduce the formula 𝐴 = {𝑥 ∣ 𝑥 = 𝑥}
to ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 = 𝑥). For a class and a set variable symbol 𝐴, it is necessary to be able to expand
each of the formulas 𝑥 ∈ 𝐴, 𝑥 = 𝐴, 𝐴 ∈ 𝑥, and 𝐴 = 𝑥 into a formula without an occurrence of a
class.
Reference J. R. Shoenfield, "Axioms of Set Theory", p 339.

Judging by the above classes must not appear on the outside in ZF, but internal usage is okay.

There is still a bit more to say here, I think. Using axioms in a formal system is a steady process of narrowing down its possibilities. Right in the beginning, the system is open for any future development. At the point where df-cleq is introduced, either coming first, or after df-clab is known, nothing is fixed about the particular set theory you finally want to arrive at. In the comment to df-cleq its perhaps helpful to note the goal, so readers never loose contact to the big picture, but the motivation for narrowing down the formal system is in my experience often resolving a far more local ambiguity. In the case of df-cleq the yet undefined "A = B" should resemble equality by being at least an equivalence relation, and it formally and factually should extend axextb.

[wlammen]

A quote from @LegionMammal978

In service of this goal, classes in set.mm are not interpreted their own objects with possibly-strange semantics, but simply "wff (meta)variables in disguise". When we write A = B in set.mm, we are not attempting to make any statements about "class objects", nor about their distinguishability: we are only making statements about the formula A. x ( x e. A <-> x e. B ) (for a dummy setvar x), no more and no less."

I am not sure whether proper classes, in a philosophical sense, do not qualify as "objects". Metamath handles formulas, irrespective of any interpretation. A class variable is a very simple formula, the class of all sets a more elaborate one. So why should a formula denoting a class not depict an object, either manifesting an idea, or even an interpretation then? This is perhaps a matter of taste. I personally lean towards speaking of a proper class as an object "of interest". On the other hand there is the ∃𝑥 quantifier that formally applies only to set variables. Does in your mind only something that exists (given the usual interpretation) qualify as an object? Then, strictly speaking, only set variables exist, and hence are objects.

The usual notion of equality, besides being an equivalence relation, includes a separate property I know as Leibniz's law. Wikipedia also names it "Axiom of Substitution" (beware it is NOT ax-12): (a = b) => (f(a) = f(b)). f is an arbitrary formula expressing objects based an a variable. In FOL, since you can only substitute one set variable for the other, in essence ax-7 covers Leibniz's law. What I coined indistinguishability goes a bit beyond Leibniz's law: We want well-formed formulas be equivalent, if one is the other with a replaced by b, under the assumption a = b. In Metamath's FOL I know three aspects, or implementations of it:

1. For a primitive operation between set variables (in FOL only = and ∈) this is guaranteed by axioms: ax-7 for equality and ax-8, ax-9 for membership.

2. Implicit substitution. Here indistinguishability using a particular wff is assumed by hypothesis. Most theorems using this hypothesis then state that quantifications over the repective set variable are equivalent.

3. ax12v. This variant of ax-12 allows a proof of theorem sbequ12, more or less converting Leibniz's law to well formed formulas.

Again, equality, as explained to the public by Wikipedia, needs this property. So why exactly do you want to allow classes "A = B" to somehow be distinguishable? This is a dangerous path, as it will not meet the expectations of readers.

[wlammen]

Quotes from @LegionMammal978

... but the question of axioms vs. definitions is all about our interpretations.

Otherwise every new wff construction would be a true axiom, since it similarly adds a new symbol which may inherently have all sorts of strange semantics until we constrain it.

The way Metamath uses definitions is to my knowledge always the same. It introduces one expression not used before, and explains it fully with previous material. In general the new expression is found on the left hand side of an equation or bi-conditional, its explanation on the right. Even df-bi, not conforming to this, still allows you to fully retrieve the truth table of a bi-conditional. So, one property of definitions is that they render the defined expression eliminable, and that differs it again from axioms.

By contrast, df-cleq introduces two undefined expressions, namely A = B and x ∈ A. Both, to my knowledge, stay undefined, which hinders full elimination of both. Of course, one can trace back "A = B" to expressions "x ∈ A", but this is not sufficient. As I stated in one of my answers before, ZF requires you to be able to eliminate both of them. I depicted some problems around eliminating x ∈ A in this answer #4993 (comment). You somehow have to constrain the flexibility of the class variable A and limit it to class builders cv and df-clab. This is either an axiom, or enforced by the verification process of Metamath. And then eliminating class variables in an abstract class opens a can of worms, which I don't see through at the moment.

To put it another way, I disagree with the statement: In practice, however, the more direct and fruitful approach is not to construct class equality from membership, but to treat equality itself as axiomatic.

Okay, it is certainly possible to eliminate "x = A" in df-clel, but that does not look nice. And df-clel does not constrain x ∈ A in any way. It uses it, constraining the only syntactically known A ∈ B, so again it is an axiom, no definition. Anyway, the current version of set.mm introduces df-cleq and df-clel in exactly this order and form, so your critics apply to not only my PR, but also to the original.

[wlammen]

you argue that A = B is a more fundamental concept than x e. A,

No, I don't think so. Both A = B and A e. B can be traced back to x e. A (by df-cleq and df-clel), that's why a class builder df-clab has its particular form.

As for ceqsal1t I think you are right. I tried to tackle the problem of when a class is also a set, and ceqsal1t is not good enough to provide an answer here. It seems E. x x = A is the "set builder". Being able to assign a class to a set variable is a very suggestive solution. Given that x = A is based on x e. A which is not fully defined, the answer to what classes are sets (and exist in ZF) is to some extent open. I can prove ( x = A -> E. y y = A ) with y, A disjoint, and the ax12v2 equivalent ( x = A -> ( ph -> A. y ( y = A -> ph ) ) ).

Why am I looking at sets at all? The general equation A = B has two specializations, x = A and x = y. In preparation for a possible new comment to df-cleq I tried to figure out the role these specializations play. For sets A fulfilling E. x x = A all axioms containing = in their formula ax-6, ax-7 ax-8, ax-9 and ax12v2 can be shown to hold.

[LegionMammal978]

First off, I'd like to note that it's not within my power to approve or deny changes to mathboxes. I'm mainly just taking this chance to make my own comments about the reordering proposal.

Having thought about it further, I've become sympathetic to your idea that df-clab is 'secondary' to df-cleq and df-clel, and could just as easily be placed after the two. This is mainly because instead of relying on df-clab to eliminate all possible x e. A instances, we could just as easily write 'direct' definitions of class constructs, e.g., $d x A $. $d x B $. $a |- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) ) $. in place of df-in.

The big problem is, doing it this way would greatly complicate the process of interpreting theorems in set.mm. The ultimate purpose of set.mm (and the Metamath language around it) is that for each Metamath theorem written in set.mm, there is a corresponding theorem scheme written in the language of set theory. For our purposes, the "language of set theory" is an object language with variables v1, v2, v3, ..., relations = and e., and connectives ->, -., and A.. (Of course, the language is slightly different for iset.mm.)

For example, dfnul4 |- (/) = { x | F. } corresponds to the set-theoretic scheme |- A. y ( [ y / z ] ( [ z / w ] w = w /\ -. [ z / v ] v = v ) <-> [ y / x ] F. ), with the remaining FOL connectives expanded, and the metavariables substituted for any set of object-language variables permitted by the DV conditions.

But now, let's take the theorem eqid |- A = A. What is the corresponding theorem scheme in set theory? If every class constructor has its own meaning for x e. A (as in my 'direct' version of df-in above), then in order to collect every corresponding set-theory statement, we must scrounge around for every class definition in the file. But if all class constructors boil down to cv or cab, we have an easy answer: we end up with the union of the two schemes |- x = x and |- A. y ( [ y / x ] ph <-> [ y / x ] ph ), where ph can be substituted for any object-language wff distinct from y.

So since cab-based class definitions are quite general and are sufficient to encompass all definable wffs, we might as well insist that cv or cab be the only things that a class can expand to when interpreting a set.mm theorem. Under this model, x e. A is not a primitive: it is simply the union of x e. y or x e. { y | ph }. df-clab completes the definition of x e. A, and df-cleq and df-clel are definitions built on the defined notion x e. A. (This has the annoying oddity that if we want to eliminate all x e. A instances while staying within the Metamath metalanguage, we must write several versions of each axiom and theorem, choosing either cv or cab for each class variable.)

Of course, this all presupposes that every class is still a "wff in disguise": part of your suggestion is that class variables may be substituted by things that aren't simply a "wff in disguise" in this way, so that they cannot be simply defined as a class abstraction. But this would defeat the entire purpose of having definitions be eliminable, since it would introduce proof steps that cannot be translated into the object language of set theory. This would be especially problematic if it were non-conservative, and it could create new theorems about setvars that could not be proven with set theory alone. Recall that one of the big ideas of set.mm is that "ZFC is all you need!"

You describe the philosophy of "narrowing down" new symbols with axioms in Metamath, but this doesn't account for the process of interpreting definitions in an object language, which requires that newly-defined symbols outside the object language be completely eliminable in any wff context. Recall that definitions vs. axioms is entirely foreign to the internal nature of the raw Metamath language.

---

Anyway, to try to respond to your finer points in more detail:

1. Most of the combinations x = y, x = A, A = x, A = B, x e. y, x e. A, A e. x, A e. B can be eliminated, with two exemptions x e. y and x e. A (well if you have x e. A then x e. y is given as well). They are essentially undefined, and since they are, you not only can assign to them any meaning you like, you can establish a new grammar around them, so they behave in a way unexpected in set theory. For instance, you may think of a class having an extra property like a color (or colors be also classes), that you somehow can access by a notation different from { x | ph }.

Anything on the Metamath level can have extra grammars with their own properties. We could write something dumb like

$[ set.mm $]
$c red blue $.
ax-red $a red T. $
ax-blue $a blue ( ph -> ph ) $.
${
  ax-nredblue.1 $e red ph $.
  ax-nredblue.2 $e blue ph $.
  ax-nredblue $a |- F. $.
$}

This disrespects the logical equivalence |- ( T. <-> ( ph -> ph ) ), but is still perfectly conservative. So the possibility of extra properties on the Metamath level doesn't mean much per se. And we can't add extra properties on the semantically-meaningful level without breaking elimination into set theory. (If you do really want extra properties in a defined class, you can just as easily use an ordered pair or similar within the theory, as we do for algebraic structures, which are ordinary ZFC functions that yield their components when called with an index.)

2. As a remedy you might now demand that no extra class builder besides cv and df-clab exists. This helps with the color of classes misconception. But it leaves open whether all classes have a sensible notation as { x | ph }. It is suggested by NM to use A = { x | x e. A } here, but that looks fishy to me. If I apply df-clab to x e. { x | x e. A }, I end up with x e. A again, so this is NOT a valuable replacement for an arbitrary class A in my eyes. You might then demand that ph is an expression free of class variables, but, for one, I know no way to formulate this condition in set.mm, and second, I see a murky field around countability. If ph is a usual expression made up of basic notations ->, -., A., = and e. there are only countable many of them. It is known that the real numbers is a set of more than countable sets, so some are NOT expressible in this way.

I think that "suggestion" is simply a way to convert 'direct' definitions such as |- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) ) into cab-based definitions such as |- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }. You aren't supposed to literally write A = { x | x e. A }, but replace the x e. A with the definition for the particular construct.

As for "whether all classes have a sensible notation as { x | ph }", we fundamentally can't break that assumption for any class without breaking eliminability into the language of set theory, which is one of the big principles of set.mm.

As for countability concerns, it's true that a written class expression can only correspond to a countable number of wffs in the object theory, under the standard interpretation. But a class expression can depend on setvars, such as { x } depending on x, and those setvars may have uncountably many possible values. So one may say that there are uncountably many values for "classes with parameters".

Is "set theory with classes" a standing term among experts excluding ZF? If so, I am unaware of it, and I apologize for misleading. Maybe "set theory using a notation of classes" would have been more appropriate.

I'm no expert either, but it's always important to know whether classes are quantifiable objects (as in NBG), or simply syntax constructions. NBG is actually considered a conservative extension of ZFC, in that all provable statements with only set variables can be proven without class variables. But it also includes new statements such as the Axiom of Global Choice that are not directly eliminable into the language of set theory. Eliminating its usage in proofs takes some advanced metatheoretical rewriting, which is contrary to Metamath's goal of external simplicity. Hence the aversion to non-eliminable class constructions.

I am not sure whether proper classes, in a philosophical sense, do not qualify as "objects". Metamath handles formulas, irrespective of any interpretation. A class variable is a very simple formula, the class of all sets a more elaborate one. So why should a formula denoting a class not depict an object, either manifesting an idea, or even an interpretation then? This is perhaps a matter of taste. I personally lean towards speaking of a proper class as an object "of interest". On the other hand there is the ∃𝑥 quantifier that formally applies only to set variables. Does in your mind only something that exists (given the usual interpretation) qualify as an object? Then, strictly speaking, only set variables exist, and hence are objects.

Well, back in the day, people wanted to be extremely liberal with what counted as an "object" and what counted as a "set" of objects. To quote a translation of Cantor, "By an 'aggregate' [set] we are to understand any collection into a whole $M$ of definite and separate objects $m$ of our intuition or our thought," which is about as broad as you can philosophically get. But then some years later, Russell published his famous paradox, presenting a collection of objects that cannot be a set. So that definition couldn't work.

If we want a meaningful axiomatic set theory, we must adopt a domain of discourse, and restrict what objects are sets and what objects can be included in sets. We can indeed think up a collection of "all classes", containing all collections of objects we can think of defining and separating, but there's no way to stuff all its properties into a formal language. (Perhaps we might come up with a few ideas from definiteness and separateness, such as transitivity of equality, but the resulting theory will be woefully incomplete.)

In the case of set.mm, we build our theory on the ZFC axioms, whose domain of discourse is the sets alone. We can write theorems talking about individual classes, but only insofar as they are a 'fiction' that can be directly eliminated into definable properties of sets. It's possible to fully add 'class' objects to our domain of discourse, as NBG does, but this would greatly complicate eliminability into ZFC. One of the major points of this project is that "ZFC is enough", and we don't really need class objects for that.

The usual notion of equality, besides being an equivalence relation, includes a separate property I know as Leibniz's law. Wikipedia also names it "Axiom of Substitution" (beware it is NOT ax-12): (a = b) => (f(a) = f(b)). f is an arbitrary formula expressing objects based an a variable. In FOL, since you can only substitute one set variable for the other, in essence ax-7 covers Leibniz's law. What I coined indistinguishability goes a bit beyond Leibniz's law: We want well-formed formulas be equivalent, if one is the other with a replaced by b, under the assumption a = b.

Personally, I like to call this property "indiscernibility of identicals", at least on the semantic level. But to each their own.

Again, equality, as explained to the public by Wikipedia, needs this property. So why exactly do you want to allow classes "A = B" to somehow be distinguishable? This is a dangerous path, as it will not meet the expectations of readers.

I don't. If we're citing Wikipedia, I'll note that a class is "a collection of sets... that can be unambiguously defined by a property that all its members share". In set.mm, I want a class to be specified by its defining property. So if two classes A and B have equivalent defining properties for their members, then they are equal, and vice versa. As it happens, this is precisely expressed by df-cleq, assuming that x e. A has the meaning of "the value of x satisfies the defining property of A".

The only way that df-cleq wouldn't fully capture class equality is if class constructions could have non-extensional "colors" on the Metamath level, as you call them. But I do not support those in the general set.mm, since they would break eliminability. (And if you do want tagged classes, there are ways to do that inside the theory.)

By contrast, df-cleq introduces two undefined expressions, namely A = B and x ∈ A. Both, to my knowledge, stay undefined, which hinders full elimination of both. Of course, one can trace back "A = B" to expressions "x ∈ A", but this is not sufficient. As I stated in one of my answers before, ZF requires you to be able to eliminate both of them.

How so? If all classes are extensional (as they currently are, under the rules for definitions), then df-cleq is sufficient for eliminating every A = B instance into x e. A and x e. B. It's only if classes have non-extensional "colors" but we still want indiscernibility of identicals that both need their own definition schemes.

And then eliminating class variables in an abstract class opens a can of worms, which I don't see through at the moment.

As I mentioned above, for each statement involving a class variable A, one can introduce two new statements, one with x in place of A, and the other with { x | ph } in place of A. Recursively repeat this for all class variables in the statement. One can avoid the exponential blowup by only using { x | ph } and performing some rewriting in the style of cvjust, but this can add some additional axioms in the general case.

Okay, it is certainly possible to eliminate "x = A" in df-clel, but that does not look nice. And df-clel does not constrain x ∈ A in any way. It uses it, constraining the only syntactically known A ∈ B, so again it is an axiom, no definition. Anyway, the current version of set.mm introduces df-cleq and df-clel in exactly this order and form, so your critics apply to not only my PR, but also to the original.

I do not mean to use df-clel to define x e. A. I mean that its definition is completed by df-clab for the purposes of set.mm, so A = B is fully defined by df-cleq, and we do not need to "treat equality itself as axiomatic".

No, I don't think so. Both A = B and A e. B can be traced back to x e. A (by df-cleq and df-clel), that's why a class builder df-clab has its particular form.

I'm only referring to your comment "In practice, however, the more direct and fruitful approach is not to construct class equality from membership, but to treat equality itself as axiomatic." "Treating [class] equality itself as axiomatic" would only be necessary if we added non-extensional class colors, which would break eliminability.

[wlammen]

The big problem is, doing it this way would greatly complicate the process of interpreting theorems in set.mm.

I am not in favor of adding definitions in the form df-clab is structured. Its structure is a first time problem arising from a limited environment still not very expressive. Its form is motivated by what df-cleq and df-clel do not define themselves, namely the term x e. A. Later one should use equality instead, after the idea of an abstract class is available.

Of course, this all presupposes that every class is still a "wff in disguise"

and those setvars may have uncountably many possible values.

The basic idea of a variable is that it stands for something concrete, though often unspecified. What is the pool of contents, or interpretations, you can substitute variables with? For a class variable class builders make up this pool. It may allow future additions. In such a case you cannot perform a full case study, and a variable remains always, to some extent, undefined. Consequently, elimination of a class variable is impossible (unless you know something about its contents, of course).

If you want class variables be eliminable, you first need a limited pool, allowing you to handle each branch individually. Fortunately, in set theory nothing besides cv and df-clab seems necessary. Then the next question about elimination of class variables is: Can all sets be expressed as class abstractions, free of class variables? Using { x | x e. y }, for example? Maybe. Classes? I don't think so. For ZF you should then limit classes to those having a class variable free definition. How is this enforced?

Set variables in Metamath have no set builder, so no pool exists. Later on assignment serves this role a bit, but that is not the same. You are unable to eliminate, let alone define, set variables.

All of this need not be clarified in the early bootstrapping phase given by the range of df-cleq, df-clel and df-clab. Simply assume the worst case, an unlimited pool, and check the formalism stays valid. Then it will hold, no matter how you later "narrow down" set theory to what you have in mind.

How so? If all classes are extensional ...

At the time df-cleq is introduced, both A = B and x e. A are just syntactically valid expressions, no definitions given, not even when df-clab is known. x e. A may even have the reverse meaning: A is a member of x, for A not a set (however you find out what a set is). If you can prove all class variables can be replaced with an abstract class, then x e. A has a meaning. But where is the proof? Or axiom? The colors are a sort of academic counter example, that somehow must be ruled out.

It seems I am now able to formulate many ideas in a more precise way. In the past I sometimes just felt uneasy, and came up with the "colors" of classes idea for a possible counter example for either having a pool of 3 class builders, or an equality without indistinguishability.

Many thanks for your support.

---

The motivation of this PR is to point out all the hidden assumptions behind the definitions and axioms presented in the early phase of set theory, and use them in a rewrite of comments.

[LegionMammal978]

I am not in favor of adding definitions in the form df-clab is structured. Its structure is a first time problem arising from a limited environment still not very expressive. Its form is motivated by what df-cleq and df-clel do not define themselves, namely the term x e. A. Later one should use equality instead, after the idea of an abstract class is available.

Of course, I'm not in favor of generally adding definitions in that form, no more than I'd be in favor of copying df-bi-style |- -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) definitions all over the propositional logic section. I just mean that if we did add more class definitions in that form, then they would be perfect examples of x e. A substitutions not based on cv or cab, which is very similar to what you have been describing.

But as long as we can write all those definitions within Metamath, they always tie a class construction to a definable wff that could've been written with cab instead, so we don't gain any expressive power. And if we demand (as we currently do) that all x e. A eliminations are based on cv or cab, then that greatly simplifies the elimination process. Meanwhile, if we couldn't write some of those class definitions as a wff within Metamath, then simple elimination into the object language of =, e., ->, -., A. would be impossible.

The basic idea of a variable is that it stands for something concrete, though often unspecified. What is the pool of contents, or interpretations, you can substitute variables with? For a class variable class builders make up this pool. It may allow future additions. In such a case you cannot perform a full case study, and a variable remains always, to some extent, undefined. Consequently, elimination of a class variable is impossible (unless you know something about its contents, of course).

On the Metamath level, you can substitute a class variable for a cv instance, a cab instance, a defined class construct, or another class variable. On the level of interpretation, we do want elimination of a class variable to be possible, and that's why we do demand that every class definition come back to cv or cab.

How do we demand this? With the definition checker. If every class construction after df-clab is defined as |- Foo = Bar, then since there are only finitely many class definitions, each of which can only refer to previous constructions, we'll eventually reach cv or cab if we keep expanding.

If you want class variables be eliminable, you first need a limited pool, allowing you to handle each branch individually. Fortunately, in set theory nothing besides cv and df-clab seems necessary. Then the next question about elimination of class variables is: Can all sets be expressed as class abstractions, free of class variables? Using { x | x e. y }, for example? Maybe.

I'm glad we agree there must be a definite pool if we want eliminability. For set.mm, this pool is direct setvars from cv and class abstractions from cab. (During elimination, we technically don't ever need to rewrite a cv setvar as a class abstraction. We only need to know that they're equivalent when we check conservativity.)

Classes? I don't think so. For ZF you should then limit classes to those having a class variable free definition. How is this enforced?

I suppose your question is, "If we can define classes in terms of other class variables A, B, C, ... when substituting on the Metamath level, then how can class abstractions without class variables be sufficient when eliminating?" But that's always how elimination works: it can be narrower than Metamath substitution. E.g., when (metatheoretically) eliminating setvar metavariables, we only eliminate them with object-language variables, not with other setvar metavariables. Similarly, when eliminating class variables, we only eliminate them with cvs and cabs with object-language wffs.

So then the next question is, what is the relation between substitution and elimination? As I understand it, the important rule is, "If a Metamath statement $A$ is a substitution instance of a Metamath statement $B$, then the scheme that results from eliminating $A$ is a subset of the scheme that results from eliminating $B$."

For instance, let's say that statement $B$ involves y e. B with a class variable B, and statement $A$ substitutes y e. B for y e. { x | x e. A } with a new class variable A. Then eliminating $B$ results in the union of y e. x and [ y / x ] ph, and eliminating $A$ results in the union of [ y / x ] x e. z and [ y / x ] [ x / z ] ph. Since every elimination of $A$ falls under some elimination of $B$, the rule is upheld.

As for enforcement, we first enforce with the definition checker that every class construction can be boiled down to cv and cab, so that the only remaining notion on the Metamath level is x e. A for class variables A. Then, we justify metatheoretically that the rule for elimination holds if we replace every A with y or { y | ph }. Under the "Justification" section in "The Theory of Classes", it's said that Levy wrote out the proof for eliminability and conservativity of this rewrite, but I haven't actually checked the full proof.

Set variables in Metamath have no set builder, so no pool exists. Later on assignment serves this role a bit, but that is not the same. You are unable to eliminate, let alone define, set variables.

When interpreting set.mm variables, we eliminate setvar metavariables into object-language variables $v_1$, $v_2$, $v_3$, etc. From the "Axioms vs. axiom schemes" section on the front page:

The actual language (also called the object language) of first-order logic consists of starting (or primitive or atomic) wffs (well-formed formulas) constructed from actual individual variables v₁, v₂, v₃,... connected by = and ∈ (such as "v₂ = v₄" and "v₃ ∈ v₂"), which are then used to build up larger wffs with the connectives →, ¬, and ∀ (such as "(¬ v₂ = v₄ → ∀ v₆ v₃ ∈ v₂)"). That is the complete language needed to express all of set theory and thus essentially all of mathematics. That's it; there is nothing else! There are no other variable types in the actual language; in particular there are no variables representing wffs. Each of our axiom schemes corresponds to (generates) an infinite set of such actual formulas that match its pattern. For example, "(∀ v₁ ¬ v₃ ∈ v₂ → ¬ v₃ ∈ v₂)" is an actual axiom since it matches axiom scheme ax-c5, "(∀𝑥𝜑 → 𝜑)," when we substitute "v₁" for "𝑥" and "¬ v₃ ∈ v₂" for "𝜑."

So that is the "pool" we use when eliminating setvars. Of course we can't write these within Metamath, but the Metamath language has no concept of elimination, let alone eliminable and conservative definitions. Definitions are all about the interpretation outside the Metamath language.

For class variables, the "pool" for elimination is object-language variables v_i and abstractions {v_i | 𝜑}, where 𝜑 is an object-language wff. (Or rather, the "pool" for eliminating x e. A is "v_j ∈ v_i" and "∀v_k(v_k = v_j → ∀v_i(v_i = v_k → 𝜑))".) We only need countably many class eliminations for the same reason we only need countably many setvar eliminations: there are only finitely many variables in an expression, and the uncountability only creeps in with the variable assignments when interpreting the object language. (That is, there is a two-step interpretation process, Metamath theorems → object-language schemes, then object-language variables → variable assignments. We don't need uncountability in the first step.)

All of this need not be clarified in the early bootstrapping phase given by the range of df-cleq, df-clel and df-clab. Simply assume the worst case, an unlimited pool, and check the formalism stays valid. Then it will hold, no matter how you later "narrow down" set theory to what you have in mind.

Arguably, the "narrowing-down" process for bootstrapping is only needed when we're talking about expressions that exist in the object language. The object language has = and ∈ and variables, so we must add axioms that specify their behavior. On the other hand, class variables and class constructions are supposed to be immediately eliminable from existence, so we specify how to eliminate x e. A ASAP before building up other wffs with classes. We don't want any "class axioms" to end up in the object language, but we do allow the FOL and ZFC axioms to end up in the object language.

At the time df-cleq is introduced, both A = B and x e. A are just syntactically valid expressions, no definitions given, not even when df-clab is known. x e. A may even have the reverse meaning: A is a member of x, for A not a set (however you find out what a set is). If you can prove all class variables can be replaced with an abstract class, then x e. A has a meaning. But where is the proof? Or axiom? The colors are a sort of academic counter example, that somehow must be ruled out.

Since interpretation occurs outside the Metamath language, we cannot simply write a proof about "meanings" within it. Allegedly, the proof for eliminability comes from Levy and other authors, cited within "The Theory of Classes" on the front page. But the overall proof sketch is not hard to see, it's entirely a matter of syntactic manipulations. Yet this eliminability presupposes that all substitutions of classes are ultimately cv or cab, so that's what we enforce right away with the definition checker, instead of letting everything get "narrowed down" into place.

[wlammen]

I have only little time available, so some quick remarks:

I suppose your question is, ...

I thought more along the lines { x | x e. A } when you know nothing about A.

When interpreting set.mm variables, ...

I don't want to eliminate set variables. I simply stated they can't be eliminated because there are no objects of type setvar. This was meant as an example of variables without "pool", i.e. set builders. Maybe there is room for discussions, but for me they are elementary, needed for quantification and the simple set model in FOL.

I find some remarks of you helpful with respect to the role of substitution. Assignment replaces substitution in the expression x = A, so equality must be well-behaved enough for this purpose. I can prove theorems mimicking axioms using equality in FOL, under the assumption E. x x = A following holds
ax-6ev E. x x = A
ax-7 ( x = y -> ( x = A -> y = A ))
ax-8 ( x = y -> ( x e. A -> y e. A ))
ax-9 ( x =y -> ( A e. x -> A e. y ))
ax12v2 (x = A -> ( ph -> A. z ( z = A -> ph )))

ax-13 is of no interest.

This means, all proofs of theorems that replace a setvar y by a class A, carry simply over, if 1. A contains a set; 2. no quantifier is applied to y.

---

I think it is time to rework this PR to use more of the comments here. I need time for it though, and this is limited for me, so perhaps results will need a couple of days.

Thanks for your support.