MetamathHome
| Metamath Home |
Metamath $j commands |
As noted in section 4.4.3, "Additional Information Comment ($j)", of the metamath specification, we have a way to include information in metamath proof files which are not needed for verifying, but which are useful for other tools like proof assistants, definition checkers, conversion to and from other proof formats, and the like. Although the metamath specification has some examples, it seems better to document the full list here because they aren't part of the specification in the sense of being needed for verification.
Many of these are experimental and may be lightly used in practice. We would like for this page to be the source of truth which describes the rules that the tools should implement. But don't make too many assumptions, including about whether the $j commands do anything at all in a particular situation. Contact us (for example via a github issue or the mailing list) if this documentation is incomplete.
$j syntax 'TYPECODE' ...;
State that TYPECODE is a typecode. That is, it is a constant symbol which appears in the leftmost position in statements. This form is specifically for variable typecodes, which means they have one or more $f statements and are usually omitted from HTML display. Syntax axioms (which have this typecode) should not have any repeated variables or $d or $e hypotheses.
This command is repeatable by passing a list of typecodes.
$j syntax 'SYNTAX' as 'TYPECODE';
State that SYNTAX is a logical typecode, that is, a constant symbol
which appears in the leftmost position in statements. This form is
for typecodes that are not directly used for variables but can appear
in provable statements, and any statement starting with SYNTAX should
be followed by a grammatically correct expression which parses as
an expression with typecode TYPECODE.
$j primitive 'PRIMITIVE' ...;
State that PRIMITIVE is the name of a $a statement which represents syntax which is only defined implicitly (by axioms), not by a definition.
This command is repeatable by passing a list of constructors.
$j definition 'DEFTHM' for 'SYNTAX';
Declare a theorem to be a definition. DEFTHM is a $p statement which
represents an alternative definition for the syntax represented by
the $a statement SYNTAX. The definition should have a top level
equality declared by the equality command with the definition on
the right hand side. (This command is only needed when the
definition does not immediately follow the syntax itself, which
in set.mm only occurs for df-bi. For most definitions we can
automatically infer the requisite structure.)
$j justification 'JUSTIFICATION' for 'DEFINITION';
State that the theorem called JUSTIFICATION is a justification theorem for the definition DEFINITION, as described in the section "Appendix 4: A Note on Definitions" of mmset.html
$j restatement 'AXIOM' of 'THEOREM';
This is used immediately after an axiom which exactly matches a
previous theorem statement. This is used when the full set of axioms
is redundant but there are many overlapping subsystems, so some axioms
imply the others. Theorem displays can make use of this information
to decrease the number of listed axioms. For example, if a theorem
depends on A, B, C but C can be proven from A + B, a theorem
display might say that the theorem only depends on A, B even
though it makes use of a theorem that depends on A, C which
cannot be minimized in this way.
$j usage 'THEOREM' avoids 'STATEMENT' ...;
The proof of THEOREM should not use any listed STATEMENT, directly or indirectly. Although STATEMENT will often be an axiom (for example the axiom of choice or the axiom of infinity), it can also be a theorem which this proof should avoid. Tools are encouraged to check for violations and flag them as errors.
$j type_conversions;
Adds all "type conversions" to the grammatical parser. These are
syntax axioms like class x (where x is a
variable of type setvar) that introduce no syntax but
allow conversion from one typecode to another.
$j unambiguous 'klr 5';
State that the grammar is unambiguous, verifiable using the KLR parser, with compositing depth 5.
$j garden_path 'TOKEN' 'TOKEN' ... => 'TOKEN' ...;
This is used to help the metamath-knife parser parse expressions
which can be parsed only after some lookahead. The syntax gives an
initial token sequence (possibly containing variables representing
previously parsed subexpressions), and gives a replacement parse
to consider instead. For example,
garden_path ( x e. A => ( ph ;
asserts that after parsing an initial sequence ( x e. A,
it should consider revising the parse to ( ph (that is,
reducing x e. A to a wff) if the next token does not
continue constructing a syntax form. (In this case, it could be the
start of ( x e. A |- ph ) or the x e. A
may need to be interpreted as a wff if it
is ( x e. A /\ ph ) .)
$j equality 'SYNTAX' from 'REFL' 'SYM' 'TRAN';
Register an equivalence relation. SYNTAX is the $a statement for the syntax, and REFL, SYM, and TRAN are the names of theorems (in inference form) establishing reflexivity, symmetry, and transitivity respectively.
$j congruence 'THEOREM' ...;
State that THEOREM is a congurence lemma. This should have the
form
|- a1 = b1 & ... & |- an = bn ==> |- F(a1,...,an) = F(b1,...,bn)
where each = is the appropriate equality for the type and F is
the constructor to prove the congruence about. This is only required
for primitive constructors; for definitions these theorems can be inferred.
This command is repeatable by passing a list of theorems.
$j condequality 'CONDEQ' from 'THEOREM';
This labels a declaration CONDEQ as a "conditional equality".
This is a technical definition used in the proof that equality is a
congruence; it should be a ternary constructor
CondEq(x, y, ph) which
expresses ( x = y -> ph ). The THEOREM should be a proof of
ph |- CondEq(x, y, ph), which is one of the structural
rules required for it.
$j condcongruence 'THEOREM' ...;
The THEOREM should be a proof of
CondEq(x, y, a1 = b1), ..., CondEq(x, y, an = bn)
|- CondEq(x, y, F(a1, ..., an) = F(b1, ..., bn)) for a
primitive constructor F. There should be one for every
primitive constructor. For setvar arguments to binding constructors,
there should be two versions: one has the form
CondEq(x, y, A = B) |- CondEq(x, y, F(z, A) = F(z, B))
where x,z and y,z are distinct, and the
other should have the form
CondEq(x, y, A = B) |- CondEq(x, y, F(x, A) = F(y, B))
where x,B and y,A are distinct. This is
used in the proof that equality is a congruence.
This command is repeatable by passing a list of theorems.
$j bound 'TYPECODE' ...;
State that TYPECODE is a typecode which permits binding
constructors, like the x in A. x ph
or { x | ph }. These
typecodes are required to not have any constructors.
This command is repeatable by passing a list of typecodes.
$j free_var 'SYNTAX' with 'BVAR' ...;
SYNTAX should be the name of a $a statement which defines a syntax containing the variable > VARIABLE. State that VARIABLE is free in that syntax.
Declares that variables BVAR are not binders in syntax SYNTAX,
and instead represent free variables. This is needed when SYNTAX
is a syntax constructor containing both a variable of bound typecode
and another variable, in which case the default assumption is that
the syntax is a binder like A. x ph. If the definition
of syntax foo x ph is instead x = 0 /\ ph
we want to indicate that x is not binding occurrences
in ph and x is a free variable in the
result.
$j free_var_in 'SYNTAX' with 'VAR' 'BVAR';
Declares that occurrences of variable BVAR are not bound in
VAR in syntax SYNTAX, and instead represent free variables.
This is needed when SYNTAX is a syntax constructor containing both
a variable of bound typecode and another variable, in which case
the default assumption is that the syntax is a binder like
A. x ph. If the definition of syntax foo x ph
is instead x = 0 /\ ph we want to indicate that
x is not binding occurrences in ph
and x is a free variable in the result.
This is a more specific version of free_var which points to a
specific variable VAR which BVAR does not bind, while still
allowing it to bind occurrences in other variables in the syntax.
For example if foo A x ph has definition
A = 0 /\ A. x ph we want to indicate that occurrences
of x in A are not bound, even though
x is a binding variable in the notation.
$j notfree 'NF' from 'THEOREM';
This declares NF as a "not-free" operator. The
THEOREM should be a proof of
NF(x, A), CondEq(x, y, A = B) |- A = B where = is the
appropriate equality for the typecode. It makes use of a
condequality to justify the definition.
$j natded_init 'IMP', 'AND', 'TRUE';
Sets up the basic structure for natural deduction based automation.
Expects arguments indicating the names of implication (the turnstile
symbol in natural deduction), conjunction (which is used to build
up the context of a natural deduction sequent), and true (the empty
context). This command must precede any other natded_* commands.
$j natded_assume 'THEOREM' ...;
Registers THEOREM as an "assumption" style rule. This should
have the form |- (CONJ -> A) where CONJ is
some nesting of conjunctions in which A is a member.
(There are no other requirements on these lemmas, and the automation
has free choice to use these as required, but there should at least
be A -> A available.)
This command is repeatable by passing a list of theorems.
$j natded_weak 'THEOREM' ...;
Registers THEOREM as a "weakening" style rule. This should have
the form |- (CONJ1 -> A) ==> |- (CONJ2 -> A) where
CONJ1 and CONJ2 are some nesting of
conjunctions in which all atoms of CONJ1 are elements of CONJ2.
For the empty context, either |- (T -> A) or
|- A are acceptable forms. (There are no other
requirements on these lemmas, and the automation has free choice
to use these as required, but there should at least
be A -> C |- (A /\ B) -> C and
B -> C |- (A /\ B) -> C available.)
This command is repeatable by passing a list of theorems.
$j natded_cut 'THEOREM' ...;
Registers THEOREM as a "cut" style rule. Every hypothesis and
conclusion should have the form |- (CONJ -> A) or |- A,
and it should represent some Horn clause reasoning, like
A -> B, B -> C |- A -> C, A, A -> B |- B,
A -> B, (A /\ B) -> C |- A -> C and so on. (There are no
other requirements on these lemmas, and the automation has free
choice to use these as required.)
This command is repeatable by passing a list of theorems.
$j natded_true 'TRUE' with 'THEOREM' ...;
Registers THEOREM as a natural deduction rule pertaining to
the true constant TRUE (which does not necessarily have to coincide
with the TRUE constant used for the empty context in natded_init).
These have no specified form besides the use of | (CONJ -> A) and
|- A hypotheses and conclusion, but they will generally involve
introducing true as in |- T. or |- ( A -> T. ) or eliminating
true on the left as in ( T. -> A ) |- A. (Automation has free
choice to make use of these lemmas as required, but an analogue
of tru is recommended.)
This command is repeatable by passing a list of theorems, or
it can be split into multiple commands; the 'TRUE' with part must
be repeated in this case. Multiple TRUE constants can also be
introduced by using multiple commands.
$j natded_imp 'IMP' with 'THEOREM' ...;
Registers THEOREM as a natural deduction rule pertaining to
implication IMP (which does not necessarily have to coincide
with the IMP constant used for the sequent operator in natded_init).
These have no specified form besides the use of
| (CONJ -> A) and |- A hypotheses and conclusion, but they
will generally involve introducing implication as in
(A /\ B) -> C |- A -> (B -> C) and eliminating it as in
A -> B, A -> (B -> C) |- A -> C. (Automation has
free choice to make use of these lemmas as required, but analogues
of ex and mpd are recommended.)
This command is repeatable by passing a list of theorems, or it
can be split into multiple commands; the 'IMP' with part must be
repeated in this case. Multiple IMP constants can also be
introduced by using multiple commands.
$j natded_and 'AND' with 'THEOREM' ...;
Registers THEOREM as a natural deduction rule pertaining to
conjunction AND (which does not necessarily have to coincide
with the AND constant used for the context conjunction in
natded_init). These have no specified form besides the use
of | (CONJ -> A) and |- A hypotheses and conclusion, but they
will generally involve introducing conjunction as in
A -> B, A -> C |- A -> (B /\ C) and eliminating it as in
A -> (B /\ C) |- A -> B. (Automation has free choice to
make use of these lemmas as required, but analogues of jca,
simpld and simprd are recommended.)
This command is repeatable by passing a list of theorems,
or it can be split into multiple commands; the 'AND' with part
must be repeated in this case. Multiple AND constants can also be
introduced by using multiple commands.
$j natded_or 'OR' with 'THEOREM' ...;
Registers THEOREM as a natural deduction rule pertaining to
disjunction OR. These have no specified form besides the use of
| (CONJ -> A) and |- A hypotheses and conclusion, but they
will generally involve introducing disjunction as in
A -> B |- A -> (B \/ C), and eliminating it as in
(A /\ B) -> D, (A /\ C) -> D, A -> (B \/ C) |- A -> D.
(Automation has free choice to make use of these lemmas as
required, but analogues of olcd, orcd and mpjaodan are
recommended.)
This command is repeatable by passing a list of theorems, or
it can be split into multiple commands; the 'OR' with part
must be repeated in this case. Multiple OR constants can also
be introduced by using multiple commands.
$j natded_not 'NOT' 'FALSE' with 'THEOREM' ...;
Registers THEOREM as a natural deduction rule pertaining to
negation NOT and falsity symbol FALSE. These have no specified
form besides the use of | (CONJ -> A) and |- A hypotheses
and conclusion, but they will generally involve introducing
negation as in (A /\ B) -> F. |- A -> -. B, and eliminating
it as in A -> B, A -> -. B |- A -> C, and eliminating
falsity via A -> F. |- A -> B. (Automation has free choice
to make use of these lemmas as required, but analogues of inegd,
pm2.21dd and falimdd are recommended.)
This command is repeatable by passing a list of theorems, or it
can be split into multiple commands; the 'NOT' 'FALSE' with part
must be repeated in this case. Multiple NOT and FALSE constants
can also be introduced by using multiple commands, and a negation
can associate to multiple falsity constants and vice versa.
The theorems provided should not mention any other constructors
than the specified NOT and FALSE however (and
IMP, AND, TRUE from natded_init).
Although it may be difficult to keep an up to date list of which tools use which $j commands, here is the information we currently have. Please contact us (for example via github issue or mailing list) if you find inaccuracies in this list.
This page is dedicated to the public domain through the Creative Commons license CC0, to maximize the availability of this page's information.