Theorem wl-cleq-2 37483

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: Well-formed formulas**

The parser that processes strictly formatted Metamath text with logical or mathematical content constructs its grammar dynamically. New syntax rules are added on the fly whenever they are needed to parse upcoming formulas. Only a minimal set of built-in rules - those required to introduce new grammar rules - is predefined; everything else must be supplied by set.mm itself as syntactic units identified by the first-stage parser. Text regions beginning with the tokens "$c" or "$v", for example, provide such grammar extensions.

We will outline the extension process used when introducing an entirely new concept that cannot build on any prior material. As a simple example, we will trace here the steps involved in defining formulas, the expressions used for hypotheses and statements - a concept first-order logic needs from the very beginning to articulate its ideas.

1. **Introduce a type code**

To mark new formulas and variables later used in theorems, the constant "wff" is reserved. It abbreviates "well-formed formula", a term that already suggests that such formulas must be syntactically valid and therefore parseable to enable automatic processing.

2. **Introduce variables**

Variables with unique names such as 𝜑, 𝜓, ..., intended to later represent formulas of type "wff". In grammar terms, they correspond to non-terminal symbols. These variables are marked with the type "wff". Variables are fundamental in Metamath, since they enable substitution during proofs: variables of a particular type can be consistently replaced by any formula of the same type. In grammar terms, this corresponds to applying a rewrite rule. At this step, however, no rewrite rule exists; we can only substitute one "wff" variable for another. This suffices only for very elementary theorems such as idi 1.

3. **Add primitive formulas**

Rewrite rules describing primitive formulas of type "wff" are then added to the grammar. Typically, they describe an operator (a constant in the grammar) applied to one or more variables, possibly of different types (although at this stage only "wff" is available). Since variables are non-terminal symbols, more complex formulas can be constructed from primitive ones, by consistently replacing variables with any wff formula - whether involving the same operator or different ones introduced by other rewrite rules. Whenever such a replacement introduces variables again, they may in turn recursively be replaced.

If an operator takes two variables of type wff, it is called a binary connective in logic. The first such operator encountered is (𝜑 → 𝜓). Based on its token, its intended meaning is material implication, though this interpretation is not fixed from the outset.

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

Once the biconditional connective is available for formulas, new connectives can be defined by specifying replacement formulas that rely solely on previously introduced material. Such definitions makes it possible to eliminate the definiens.

At the very beginning, however, this is not possible for well-formed formulas, since little or no prior material exists. Instead, the semantics of an expression such as (𝜑 → 𝜓) are progressively constrained by axioms - that is, theorems without proof. The first such axiom for material implication is ax-mp 5, with additional axioms following later.

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

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem wl-cleq-2

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)