Description: Disclaimer: The material presented here is just my (WL's) personal perception. I am not an expert in this field, so some or all of the text here can be misleading, or outright wrong.
This text should be seen as an exploration, rather than viewing it as set in stone, no doubt or alternatives possible.
We now introduce the notion of class abstraction, which allows us to describe a specific class, in contrast to class variables that can stand for any class indiscriminately.
A new syntactic form is introduced for class abstractions, { y | ph } , read as "the class of sets y such that ph ( y ) ". This form is assigned the type "class" in cab , so it can consistently substitute for a class variable during the syntactic construction process.
**Eliminability**
The axioms ax-wl-cleq and ax-wl-clel leave only x e. A unspecified. The definition of this class builder directly corresponds to that expression. When a class abstraction replaces the variable A and B , then A = B and A e. B can be expressed in terms of these abstractions.
For general eliminability two conditions are needed:
1. Any class builder must replace x e. A with an expression containing no class variables. If necessary, class variables must be eliminated via a finite recursive process.
2. There must only be finitely many class builders. If a class variable could range over infinitely many builders, eliminability would fail, since unknown future builders would always need to be considered.
Condition (2) is met in set.mm by defining no class builder beyond cv and df-clab . Thus we may assume that a class variable represents either a set variable, or a class abstraction:
a. If it represents a set variable, substitution eliminates it immediately.
b. If it equals a set variable x , then by cvjust it can be replaced with { y | y e. x } .
c. If it represents a proper class, then it equals some abstraction { x | ph } . If ph contains no class variables, elimination using ph is possible. The same holds if finite sequence of elimination steps renders ph free of class variables.
d. It represents a proper class, but ph in { x | ph } still contains non-eliminable class variables, then eliminability fails. A simple example is { x | x e. A } . Class variables can only appear in fundamental expressions A = B or A e. B , Both can be reduced to forms involving z e. A . Thus, in the expression z e. { x | x e. A } , we still must eliminate A . Applying df-clab reduces it back to z e. A , returning us to the starting point.
Case (d) shows that in full generality, a class variable cannot always be eliminated, something Zermelo-Fraenkel set theory (ZF) requires. If the universe contained only finitely many sets, a free class variable A could be expressed as a finite disjunction of possiblities, hence eliminable. But in ZF's richer universe, in a definition of an unrestricted class variable A = { x | ph } the variable ph will contain A in some way, violating condition (1) above. Thus constraints are needed. In ZF, any formula containing class variables assumes that non-set class variables can be be replaced by { x | ph } where ph itself contains no class variables. There is, however, no way to state this condition in a formal way in set.mm.
Class abstractions themselves, however, can be eliminated, so df-clab is a definition.
**Definition checker**
How can case (d) be avoided? A solution is to restrict generality: require that in the definition of any concrete class abstraction { x | ph } , the formula ph is either free of class variables or built only from previously defined constructions. Such a restriction could be part of the definition checker.
In practice, the Metamath definition checker requires definitions to follow the specific pattern " |- { x | ph } = ... ". Although df-clab does not conform to this pattern, it nevertheless permits elimination of class abstractions. Eliminability is the essential property of a valid definition, so df-clab can legitimately be regarded as one.
For further material on the elimination of class abstractions, see BJ's work beginning with eliminable1 and one comment in https://github.com/metamath/set.mm/pull/4971.
(Contributed by Wolf Lammen, 28-Aug-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wl-df-clab |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-clab |