Description: Metamath handles substitution uniformly. Any expression may replace a variable provided that their types are compatible and that no substituting expression contains a set variable prohibited by a distinct variable condition.
The axioms are formulated so that every such substitution is valid when the side conditions are satisfied. Consequently, every theorem derived from the axioms inherits the same substitution property. This agrees with standard mathematical practice, where substitution is unrestricted apart from type and freshness requirements.
Definitions introduce abbreviations for expressions represented by their definiens, usually the right-hand side of a defining biconditional. When a definition contains dummy variables, however, the definiens is not uniquely determined by the definiendum, since the names of fresh bound variables do not appear in the definiendum. Definitions of this kind are meaningful only if the particular names chosen for dummy variables are irrelevant.
In ordinary logic and mathematics, renaming fresh bound variables (alpha-renaming) is regarded as insignificant. Metamath's substitution mechanism reflects this principle, and therefore definitions must also respect it. Early versions of this database relied on this convention implicitly. Beginning in 2023, definitions involving dummy variables were accompanied by justification theorems (for example, rename-sb ) showing that alpha-renaming the definiens yields an equivalent expression. Consequently, different choices of dummy variable names cannot produce equivalences that are not already derivable within the formal system.
Metamath records not only proofs but also the list of axioms on which they depend. Since definitions are intended merely as abbreviations, their use should not affect these dependency lists. Unfortunately, the simple form of definition used before 2026 did not preserve this invariance. Two instances of a definition differing only in the names of dummy variables could be used to reprove the corresponding justification theorem with unusually low axiom usage, unattainable by proofs using axioms alone. Thus the recorded dependencies could depend on whether the definition was used or expanded away.
Beginning in February 2026, definitions involving dummy variables were therefore modified to incorporate alpha-renaming explicitly. In the intermediate scheme, the corresponding justification theorem was added as a hypothesis of the definition, ensuring that every use of the definition inherited the axioms needed to establish the renaming property. This eliminated artificial reductions in dependency lists.
Using the alpha-renaming property as an external hypothesis is, however, not ideal. A better approach is to encode the property directly in the definiens itself. This preserves the invariance of axiom dependencies while allowing reductions that are impossible with the hypothesis-based form.
Formal justifications for this improved definition scheme are given in just1-df , just2-df , and just3-df . An implementation is provided by definition df-sb and the theorems that follow, where the underlying techniques may be studied in greater detail. (Contributed by Wolf Lammen, 12-Jun-2026) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | justify-df.1 | |- ph |
|
| Assertion | justify-df | |- ph |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | justify-df.1 | |- ph |