Metamath Proof Explorer


Theorem conventions

Description:

Here are some of the conventions we use in the Metamath Proof Explorer (MPE, set.mm), and how they correspond to typical textbook language (skipping the many cases where they are identical). For more specific conventions, see:

The challenge of varying mathematical conventions



We try to follow mathematical conventions, but in many cases different texts use different conventions. In those cases we pick some reasonably common convention and stick to it. We have already mentioned that the term "natural number" has varying definitions (some start from 0, others start from 1), but that is not the only such case.

A useful example is the set of metavariables used to represent arbitrary well-formed formulas (wffs). We use an open phi, φ, to represent the first arbitrary wff in an assertion with one or more wffs; this is a common convention and this symbol is easily distinguished from the empty set symbol. That said, it is impossible to please everyone or simply "follow the literature" because there are many different conventions for a variable that represents any arbitrary wff. To demonstrate the point, here are some conventions for variables that represent an arbitrary wff and some texts that use each convention:

Distinctness or freeness



Here are some conventions that address distinctness or freeness of a variable:

There is a general technique to replace a $d x A or $d x ph condition in a theorem with the corresponding F/_ x A or F/ x ph ; here it is. |- T[x, A] where $d x A, and you wish to prove |- F/_ x A => |- T[x, A]. You apply the theorem substituting y for x and A for A , where y is a new dummy variable, so that $d y A is satisfied. You obtain |- T[y, A], and apply chvar to obtain |- T[x, A] (or just use mpbir if T[x, A] binds x). The side goal is |- ( x = y -> ( T[y, A] <-> T[x, A] ) ) , where you can use equality theorems, except that when you get to a bound variable you use a non-dv bound variable renamer theorem like cbval . The section mmtheorems32.html#mm3146s also describes the metatheorem that underlies this.

Additional rules for definitions

Standard Metamath verifiers do not distinguish between axioms and definitions (both are $a statements). In practice, we require that definitions (1) be conservative (a definition should not allow an expression that previously qualified as a wff but was not provable to become provable) and be eliminable (there should exist an algorithmic method for converting any expression using the definition into a logically equivalent expression that previously qualified as a wff). To ensure this, we have additional rules on almost all definitions ($a statements with a label that does not begin with ax-). These additional rules are not applied in a few cases where they are too strict ( df-bi , df-clab , df-cleq , and df-clel ); see those definitions for more information. These additional rules for definitions are checked by at least mmj2's definition check (see mmj2 master file mmj2jar/macros/definitionCheck.js). This definition check relies on the database being very much like set.mm, down to the names of certain constants and types, so it cannot apply to all Metamath databases... but it is useful in set.mm. In this definition check, a $a-statement with a given label and typecode |- passes the test if and only if it respects the following rules (these rules require that we have an unambiguous tree parse, which is checked separately):

  1. The expression must be a biconditional or an equality (i.e. its root-symbol must be <-> or =). If the proposed definition passes this first rule, we then define its definiendum as its left hand side (LHS) and its definiens as its right hand side (RHS). We define the *defined symbol* as the root-symbol of the LHS. We define a *dummy variable* as a variable occurring in the RHS but not in the LHS. Note that the "root-symbol" is the root of the considered tree; it need not correspond to a single token in the database (e.g., see w3o or wsb ).

  2. The defined expression must not appear in any statement between its syntax axiom ($a wff) and its definition, and the defined expression must not be used in its definiens. See df-3an for an example where the same symbol is used in different ways (this is allowed).

  3. No two variables occurring in the LHS may share a disjoint variable (DV) condition.

  4. All dummy variables are required to be disjoint from any other (dummy or not) variable occurring in this labeled expression.

  5. Either
    (a) there must be no non-setvar dummy variables, or
    (b) there must be a justification theorem.

    The justification theorem must be of form |- ( definiens root-symbol definiens' ) where definiens' is definiens but the dummy variables are all replaced with other unused dummy variables of the same type. Note that root-symbol is <-> or = , and that setvar variables are simply variables with the setvar typecode.

  6. One of the following must be true:
    (a) there must be no setvar dummy variables,
    (b) there must be a justification theorem as described in rule 5, or
    (c) if there are setvar dummy variables, every one must not be free.

    That is, it must be true that ( ph -> A. x ph ) for each setvar dummy variable x where ph is the definiens. We use two different tests for nonfreeness; one must succeed for each setvar dummy variable x . The first test requires that the setvar dummy variable x be syntactically bound (this is sometimes called the "fast" test, and this implies that we must track binding operators). The second test requires a successful search for the directly-stated proof of ( ph -> A. x ph ) Part c of this rule is how most setvar dummy variables are handled.

Rule 3 may seem unnecessary, but it is needed. Without this rule, you can define something like

       cbar $a wff Foo x y $.
       ${ $d x y $. df-foo $a |- ( Foo x y <-> x = y ) $. $}
and now "Foo x x" is not eliminable; there is no way to prove that it means anything in particular, because the definitional theorem that is supposed to be responsible for connecting it to the original language wants nothing to do with this expression, even though it is well formed.

A justification theorem for a definition (if used this way) must be proven before the definition that depends on it. One example of a justification theorem is vjust . Definition df-v |- _V = { x | x = x } is justified by the justification theorem vjust |- { x | x = x } = { y | y = y } . Another example of a justification theorem is trujust ; Definition df-tru |- ( T. <-> ( A. x x = x -> A. x x = x ) ) is justified by trujust |- ( ( A. x x = x -> A. x x = x ) <-> ( A. y y = y -> A. y y = y ) ) .

Here is more information about our processes for checking and contributing to this work:

(Contributed by the Metamath team, 27-Dec-2016) Date of last revision. (Revised by the Metamath team, 22-Sep-2022) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis conventions.1
|- ph
Assertion conventions
|- ph

Proof

Step Hyp Ref Expression
1 conventions.1
 |-  ph