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 read as an exploration rather than as definite
statements, open to doubt, alternatives, and reinterpretation.
There is a broadly shared understanding of what equality between objects expresses, extending beyond mathematics or set theory. Equality constitutes an equivalence relation among objects x , y , and z within the universe under consideration:
1. Reflexivity x = x
2. Symmetry ( x = y -> y = x )
3. Transitivity (( x = y /\ x = z ) -> y = z )
4. Identity of Indiscernables (Leibniz's Law): distinct (i.e., unequal), objects cannot share all the same properties (or attributes).
In formal theories using variables, the attributes of a variable are assumed to mirror those of the instance it denotes. For both variables and objects, items (1) - (4) must either be derived or postulated as axioms.
If the theory allows substituting instances for variables, then the equality rules for objects follow directly from those governing variables. However, if variables and instances are formally distinguished, this distinction introduces an additional metatheoretical attribute, relevant for (4).
A similar issue arises when equality is considered between different types of variables sharing properties. Such mixed-type equalities are subject to restrictions: reflexivity does not apply, since the two sides represent different kinds of entities. Nevertheless, symmetry and various forms of transitivity typically remain valid, and must be proven or established within the theory.
In set.mm formulas express attributes. Therefore, equal instances must behave identically, yielding the same results when substituted into any formula. To verify equality, it suffices to consider only primitive operations involving free variables, since all formulas - once definitions are eliminated - reduce to these. Equality itself introduces no new attribute (an object is always different from all others), and can thus be excluded from this examination.
In the FOL component of set.mm, the notion of an "object" is absent. Only set variables are used to formulate theorems, and their attributes - expressed through an unspecified membership operator - are addressed at a later stage.
Instead, several axioms address equality directly: ax-6 , ax-7 , ax-8 , ax-9 and ax-12 , and ax-13 . In practice, restricted versions with distinct variable conditions are used ( ax6v , ax12v ). The unrestricted forms together with axiom ax-13 , allow for the elimination of distinct variable conditions, this benefit is considered too minor for routine use.
Equality in FOL is formalized as follows:
2a. Equivalence Relation. Essentially covered by ax-7 , with some support of ax-6 .
2b. Leibniz's Law for the primitive e. operator. Captured by ax-8 and ax-9 .
2c. General formulation. Given in sbequ12 .
2d. Implicit substitution. Assuming Leibniz's Law holds for a particular expression, various theorems extend its validity to other, derived expressions, often introducing quantification (see for example cbvalvw ).
The auxiliary axioms ax-10 , ax-11 , ax-12 are provable (see ax10w , for example) if you can substitute y for x in a formula ph that contains no occurrence of y and leaves no remaining trace of x after substitution. An implicit substitution is then established by setting the resulting formula equivalent to ph under the assumption x = y . Ordinary FOL substitution [ y / x ] ph is insufficient in this context, since x still occurs in the substituted formula. A simple textual replacement of the token x by y in ph might seem an intuitive solution, but such operations are out of the formal scope of Metamath.
2e. Axiom of Extensionality. In its elaborated form ( axextb ), it states that the determining attributes of a set x are the elements z it contains, as expressed by z e. x . This is the only primitive operation relevant for equality between set variables.
In set.mm class variables of type "class" are introduced analoguously to set variables. Besides the primitive operations equality and membership, class builders allow other syntactical constructs to substitute for class variables, enabling them to represent class instances.
One such builder ( cv ) allows set variables to replace class variables. Another ( df-clab ) introduces a class instance, known as class abstraction. Since a class abstraction can freely substitute for a class variable, formulas hold for both alike. Hence, there is no need to distinguish between class variables and abstractions; the term class will denote "class variable or class abstraction".
Set variables, however, are treated separately, as they are not of type "class".
3a. Equivalence Relation. Axiom df-cleq , from which class versions of (1a) - (1c) can be derived, guarantees that equality between class variables form an equivalence relation. Since both class abstractions and set variables can substitute for class variables, this equivalence extends to all mixed equalities, including those with set variables, since they automatically convert to classes upon substitution.
3b. Attributes. The primitive operation of membership constitutes the fundamental attributes of a class. Axiom df-clel reduces possible membership relations between class variables to those between a set variable and a class variable. Axiom df-cleq extends axextb to classes, stating that classes are fully determined by their set members.
A class builder may introduce a new attribute for classes. An equation involving such a class instance may express this attribute. In the case of the class builder cv , an attribute called sethood is in fact introduced: A class is a set if it can be equated with some set variable.
Class abstractions supported by class builder df-clab also formally introduce attributes. Whether a class can be expressed as an abstraction with a specific predicate may be relevant in analysis. However, since theorem df-clab is a definition (and hence eliminable), these attributes can also be expressed in other ways.
3c. Conservativity. Because set variables can substitute for class variables, all axioms and definitions must be consistent with theorems in FOL. To ensure this, hypotheses are added to axioms and definitions that mirror the structure of their statement, but with class variables replaced by set variables. Since theorems cannot be applied without first proving their hypotheses, conservativity thus is enforced.
3d. Leibniz's Law. Besides equality membership is (and remains) the only primitive operator between classes. Axioms df-cleq and df-clel provide class versions of ax-8 and ax-9 , ensuring that membership is consistent with Leibniz's Law.
Sethood, being based on mixed-type equality, preserves its value among equal classes.
As long as additional class builders beyond those mentioned are only defined, the reasoning given for class abstraction above applies generally, and Leibniz's Law continues to hold.
3e. Backward Compatability. A class A equal to a set should be substitutable for a free set variable x in any theorem, yielding a valid result, provided x and A are distinct. Sethood is conveniently expressed by E. z z = A ; this assumption is added as an antecedent to the corresponding FOL theorem.
However, since direct substitution is disallowed, a deduction version of an FOL theorem cannot be simply converted. Instead, the proof must be replayed, consistently replacing x with A . Ultimately, this process reduces to the FOL axioms, or their deduction form.
If these axioms hold when A replaces x - under the above assumptions - then the replacement can be considered generally valid. The affected FOL axioms are ax-6 (in the form ax6ev ), ax-7 , ax-8 , ax-9 , ax-12 ( ax12v2 ), and to some extent ax-13 ( ax13v ). Since ZF (Zermelo-Fraenkel) set theory does not allow quantifification over class variables, no similar class-based versions of the quantified FOL axioms exist.
(Contributed by Wolf Lammen, 18-Sep-2025)
Ref | Expression | ||
---|---|---|---|
Assertion | wl-cleq-5 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfcleq |