Theorem wl-cleq-5 37495

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.

Semantics of Equality

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 𝑥, 𝑦, and 𝑧 within the universe under consideration:

1. Reflexivity 𝑥 = 𝑥

2. Symmetry (𝑥 = 𝑦 → 𝑦 = 𝑥)

3. Transitivity ((𝑥 = 𝑦 ∧ 𝑥 = 𝑧) → 𝑦 = 𝑧)

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.

Equality in First Order Logic (FOL)

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 1967, ax-7 2007, ax-8 2110, ax-9 2118 and ax-12 2177, and ax-13 2377. In practice, restricted versions with distinct variable conditions are used (ax6v 1968, ax12v 2178). The unrestricted forms together with axiom ax-13 2377, 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 2007, with some support of ax-6 1967.

2b. Leibniz's Law for the primitive ∈ operator. Captured by ax-8 2110 and ax-9 2118.

2c. General formulation. Given in sbequ12 2251.

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 2035).

The auxiliary axioms ax-10 2141, ax-11 2157, ax-12 are provable (see ax10w 2129, for example) if you can substitute 𝑦 for 𝑥 in a formula 𝜑 that contains no occurrence of 𝑦 and leaves no remaining trace of 𝑥 after substitution. An implicit substitution is then established by setting the resulting formula equivalent to 𝜑 under the assumption 𝑥 = 𝑦. Ordinary FOL substitution [𝑦 / 𝑥]𝜑 is insufficient in this context, since 𝑥 still occurs in the substituted formula. A simple textual replacement of the token 𝑥 by 𝑦 in 𝜑 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 2711), it states that the determining attributes of a set 𝑥 are the elements 𝑧 it contains, as expressed by 𝑧 ∈ 𝑥. This is the only primitive operation relevant for equality between set variables.

Equality between classes

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 1538) allows set variables to replace class variables. Another (df-clab 2715) 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 2729, 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 2816 reduces possible membership relations between class variables to those between a set variable and a class variable. Axiom df-cleq 2729 extends axextb 2711 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 1538, 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 2715 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 2715 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 2729 and df-clel 2816 provide class versions of ax-8 2110 and ax-9 2118, 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 𝐴 equal to a set should be substitutable for a free set variable 𝑥 in any theorem, yielding a valid result, provided 𝑥 and 𝐴 are distinct. Sethood is conveniently expressed by ∃𝑧𝑧 = 𝐴; 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 𝑥 with 𝐴. Ultimately, this process reduces to the FOL axioms, or their deduction form.

If these axioms hold when 𝐴 replaces 𝑥- under the above assumptions - then the replacement can be considered generally valid. The affected FOL axioms are ax-6 1967 (in the form ax6ev 1969), ax-7 2007, ax-8 2110, ax-9 2118, ax-12 2177 (ax12v2 2179), and to some extent ax-13 2377 (ax13v 2378). 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.)

Assertion

Ref	Expression
wl-cleq-5	⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem wl-cleq-5

Step	Hyp	Ref	Expression
1		dfcleq 2730	1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 206  ∀wal 1537   = wceq 1539   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2729

This theorem is referenced by: (None)