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.
**Grammars and Parsable contents**
A Metamath program is a text-based tool. Its input consists of (mostly) human-readable and editable text stored in *.mm files. For automatic processing, these files follow a strict structure. This enables automated analysis of their contents, verification of proofs, proof assistance, and the generation of output files - for example, the HTML page of this dummy theorem. A set.mm file contains many such instructions serving these purposes.
The ideas presented here focus only on specific statements: df-cleq , df-clel , and df-clab . Accordingly, only the technical concepts necessary to explain these are introduced, along with a selection of supporting theorems.
These theorems are central to a bootstrapping process that introduces objects into set.mm. We will first examine how Metamath in general creates basic new ideas from scratch, and then look at how these methods are applied specifically to classes, capable of representing objects in set theory.
This page provides a brief explanation of the general concepts behind structured text such as that found in set.mm. As noted above, set.mm is written in a form that is readable by humans. However, for Metamath this is not sufficient: the program must also verify and process set.mm automatically in order to establish a high degree of confidence in its correctness.
When a text exhibits a sufficiently regular structure, its form can be described by a set of syntax rules, known as agrammar. Such rules are composed of terminal symbols (fixed, literal elements) and non-terminal symbols, which can recursively be expanded using the grammar'srewrite rules. A program component that applies a grammar to a text is called aparser. The parser decomposes the text into smaller parts, calledsyntactic units, while often maintaining contextual information. These units may then be handed over to subsequent components for further processing, such as populating a database or generating output.
In these pages, we restrict our attention to strictly formatted material consisting of formulas with logical and mathematical content. These syntactic units are embedded in higher-level structures such as chapters, together with commands that, for example, control the HTML output.
Conceptually, the parsing process can be viewed as consisting of two stages. The top-level stage applies a simple built-in grammar to identify its structural units. Each unit is a text region marked on both sides with predefined tokens (in Metamath: keywords), beginning with the escape character "$". Text regions containing logical or mathematical formulas are then passed to a second-stage parser, which applies a different grammar. Unlike the first, this grammar is not built-in but is dynamically constructed.
In what follows, we will ignore the first stage of parsing, since its role is only to extract the relevant material embedded within text primarily intended for human readers.
(Contributed by Wolf Lammen, 18-Aug-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wl-cleq-1 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfcleq |