Theorem wl-cleq-6 37461

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.

Eliminability of Classes

One requirement of Zermelo-Fraenkel set theory (ZF) is that it can be formulated entirely without referring to classes. Since set.mm implements ZF, it must therefore be possible to eliminate all classes from its formalization.

Eliminating Variables of Propositional Logic

Classical propositional logic concerns statements that are either true or false. For example, "A minute has 60 seconds" is such a statement, as is "English is not a language". Our development of propositional logic applies to all such statements, regardless of their subject matter. Any particular topic, or universe of discourse is encompassed by the general theorems of propositional logic.

In ZF, however, the objects of study are sets - mathematical entities. The flexibility of propsitional variables is not required here. Instead, ZF introduces two primitive connectives between sets: 𝑥 = 𝑦 and 𝑥 ∈ 𝑦. ZF is concerned only with logical schemata constructed solely from these primitives. Thus, before we can eliminate classes, we must first eliminate propositional variables like 𝜑 and 𝜓. We will describe this process constructively.

We begin by restricting ourselves to propositional schemata that consist only of the primitives of ZF, without any propositional variables. Extending this step to first-order Logic (FOL) - by introducing quantifiers - yields the fundamental predicates of ZF, that is, the basic formulas expressible within it.

For convenience, we may again allow propositional variables, but under the strict assumption that they always represent fundamental predicates of ZF.

Predicates of level 0 are exactly of this kind: no classes occurs in them, and they can be reduced directly to fundamental predicates in ZF.

Introducing eliminable classes

The following construction is inspired by a paragraph in Azriel Levy's "Basic set theory" concerning eliminable classes.

A class can only occur in combination with one of the operators = or ∈. This applies in particular to class abstractions, which are the only kind of classes permtted in this step of extending level-0 predicates in ZF. The definitions df-cleq 2726 and df-clel 2808 show that equality and membership ultimately reduce to expressions of the form 𝑥 ∈ 𝐴. For a class abstraction {𝑦 ∣ 𝜑}, the resulting term amounts to [𝑥 / 𝑦]𝜑. If 𝜑 is a level-0 predicate, then this too is a level-0 expression - fully compatible with ZF.

A level-1 class abstraction is a class {𝑦 ∣ 𝜑} where 𝜑 is a level-0 predicate. A level-1 class abstraction can occur in an equality or membership relation with another level-1 class abstractions or a set variable, and such terms reduce to fundamental predicates. Predicates of either level-0, or containing level-1 class abstractions are called level-1 predicates. After eliminating all level-1 abstractions from such a predicate a level-0 expression is the result.

Analoguously, we can define level-2 class abstractions, where the predicate 𝜑 in {𝑦 ∣ 𝜑} is a level-1 predicate. Again, 𝑥 ∈ {𝑦 ∣ 𝜑} reduces to a level-1 expression, which in turn can be reduced to a level-0 one. By similar reasoning, equality and membership between at most level-2 class abstractions also reduce to level-0 expressions. A predicate containing at most level-2 class abstractions is called a level-2 predicate.

This iterative construction process can be continued to define a predicate of any level. They can be reduced to fundamental predicates in ZF.

Introducing eliminable class variables

We have seen that propositional variables must be restricted to representing only primitive connectives to maintain compatibility with ZF. Similarly, class variables can be restricted to representing class abstractions of finite level. Such class variables are eliminable, and even definitions like df-un 3936 (𝐴 ∪ 𝐵) introduce no difficulty, since the resulting union remains of finite level.

Limitations of eliminable class variables

Where does this construction reach its limits?

1. Infinite constructions. Suppose we wish to add up an infinite series of real numbers, where each term defines its successor using a class abstraction one level higher than that of the previous term. Such a summation introduces terms of arbitrary high level. While each individual term remains reducable in ZF, the infinite sum expression may not be reducable without special care.

2. Class builders. Every class builder other than cv 1538 must be a definition, making its elimination straightforward. The class abstraction df-clab 2713 described above is a special case.

Since set variables themselves can be expressed as class abstractions - namely 𝑥 = {𝑦 ∣ 𝑦 ∈ 𝑥} (see cvjust 2728) - this formulation does not conflict with the use of class builder cv 1538.

The above conditions apply only to substitution. The expression 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴} (abid1 2870) is a valid and provable equation, and it should not be interpreted as an assignment that binds a particular instance to 𝐴.

(Contributed by Wolf Lammen, 13-Oct-2025.)

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem wl-cleq-6

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

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

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 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

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

This theorem is referenced by: (None)