Theorem wl-cleq-3 37484

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 a definite statement, open to doubt, alternatives, and reinterpretation.

**Introducing a New Concept: Objects**

In wl-cleq-2 37483 we saw how the basic notion of a well-formed formula is introduced in set.mm. A similar process is used to add the notion of an object to Metamath. This process is somewhat more complex, since two variants are established in parallel: sets and the broader notion of classes, which include sets (see 3a. below). Classes, as it will turn out in Zermelo-Fraenkel set theory (ZF), serve mainly as a convenient shorthand to simplify formulas and their proofs. Ultimately, only sets - some of the classes - are intended to exist as actual objects.

In the First Order Logic (FOL) part of set.mm it is not even clear that objects must be sets at all. In principle, the universe under consideration could consist of anything - vegetables, text strings, and so on. For this reason, the type code "setvar", used for objects, is something of a misnomer. Its final meaning - and the name that goes with it - only becomes justified in later developments.

We will revisit the four basic steps presented in wl-cleq-2 37483, this time focusing on objects and paying special attention to the additional complexities that arise from extending sets to classes.

1. **Introduce type codes**

1a. Reserve a type code for classes, specifically the grammar constant "class".

1b. Reserve a type code for sets, "setvar". The name itself indicates that this type code will never be assigned to a formula that actually describes a specific set.

2. **Introduce variables**

2a. Variables with unique names such as 𝐴, 𝐵, ..., are intended to represent classes. These class variables are marked with type "class", ensuring that only formulas of type "class" can substitute for them during proofs.

2b. Variables with unique names such as 𝑎, 𝑏, ... are intended to be of type "setvar". During a substitution in a proof, a variable of type "setvar" can only be replaced with another variable of the same type. No specific formula, or object, of this type exists.

3. **Add primitive formulas**

3a. Add the rewrite rule cv 1536 to set.mm, so variables of type "setvar" also aquire type "class". In this way, a variable of "setvar" type can serve as a substitute for a class variable.

3b. Add the rewrite rules wcel 2108 and wceq 1537 to set.mm, allowing the formulas 𝐴 ∈ 𝐵 and 𝐴 = 𝐵 to be valid wff. Since variables of type "setvar" can be substituted for class variables, 𝑥 ∈ 𝑦 and 𝑥 = 𝑦 are also provably valid wff. In FOL in set.mm, only these specific formulas play a role and are therefore treated as primitive at that point. The underlying universe may not contain sets, and the notion of a class is not even be required.

Additional mixed-type formulas, such as 𝑥 ∈ 𝐴, 𝐴 ∈ 𝑥, 𝑥 = 𝐴, and 𝐴 = 𝑥 exist. When the theory is eventually narrowed down to sets and classes, the results from FOL remain valid and extend naturally to these mixed cases. In discussions, these cases will sometimes be examined individually.

4. **Specify the properties of primitive formulas**

In FOL in set.mm, the formulas 𝑥 = 𝑦 and 𝑥 ∈ 𝑦 cannot be derived from earlier material, so definitions are not possible. Instead, their basic properties are established through axioms, namely ax-6 1967 to ax-9 2118, ax-13 2380, and ax-ext 2711.

Axioms are added to specify the properties of the primitive formulas 𝐴 = 𝐵 and 𝐴 ∈ 𝐵. These must extend 𝑥 = 𝑦 and 𝑥 ∈ 𝑦 from FOL consistently and in a meaningful way. At the same time, a criterion for distinguishing sets among classes needs to be developed. Since set variables can only be substituted by other set variables, equality must allow assigning classes known to be sets to them instead.

(Contributed by Wolf Lammen, 25-Aug-2025.)

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem wl-cleq-3

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by: (None)