C:\metamath\metamath\mmcmds.c
uses the following conventions to categorize Metamath "axiom" statements ($a
):If first symbol of $a statement equals "|-"
If Label of $a statement begins with "ax-"
the statement is a Logical Axiom
Else (Label does not begin with "ax-"
the $a statement is a Definition Axiom
End-If
Else (first symbol of $a statement not equal to "|-")
the $a statement is a Syntax Axiom
End-If
These are conventions not enforced by Metamath and are tailored for the set.mm database.
wff's, sets and classes that are referred to in
theorems, logical axioms and definition axioms. In essence, a Syntax
Axiom is a statement that describes how to construct a syntactically
valid statement about a noun by combining symbols that stand for nouns,
operators and punctuation. Thus, a Syntax Axiom describes a symbol
sequence -- or, symbol pattern
-- that identifies a "thing" (an object) of the given type (the type is
given in the first symbol of the Syntax Axiom statement).set.mm
, the theorems, logical axioms and definition axioms are statements about certain things, namely wff's, sets, and classes.
Set.mm defines "wff
", "set
", and "class
" as Constants, and these
constants are coded as the first symbol on Syntax Axiom statements;
thus, assigning a Type to the symbol sequence that follows in the
statement. Logical statements that discuss the truth or provability of certain symbol sequences are coded with Type code "|-
". Formula |
Name of |
Example |
1 |
Nulls Permitted Axiom |
nullWffOk $a wff $. |
2 |
Named Typed Constant Axiom |
c0 $a class (/) $. |
> 2 |
Named Typed String Axiom |
cEmptySet $a set { } $. |
$c / ] [ $.
$v x ph A $.
cA $f class A $.
vx $f set x $.
wph $f wff ph $.
cdiv $a class / $.
wsbc $a wff [ A / x ] ph $.
wsb $a wff [ y / x ] ph $.
Q. How do"Types" relate to Axioms, Theorems and Hypotheses?wn $a wff -. ph $.
wff
" (following the "$a
" symbol), and identifies the statement labelled "wn
" as being a statement about wff
's. In English the wn statement says "the expression 'not phi' is a wff
".
wn
wff -. ph
" is the formula, and -. ph
" is the expression in the wn
statement. wff -. ph
" ( ph -> ps )
" into the formula, replacing variable ph
wff -. ( ph -> ps )
".
wff
variable can only be replaced by a wff
expression.)|-
". If the user
then created Variables and Syntax Axioms with Type code "|-
", the
resulting Logical Axioms, Theorems and Logical Hypotheses would be called
"metalogical" (logic about logic). As a practical matter, metalogical theorems can be
proved in Metamath but the "metalogician" would quite probably use
different Type codes for metalogical variables Types and Theorem Types. (In
MMJ2, a validation error is generated if the user createsVariable and Syntax
Axiom type codes that are equal to Logical Axiom, Theorem or Logical Hypothesis
Type codes.)miu.mm
is an anomaly), the Expression part of a Formula in
a Theorem, Logical Hypothesis, Logical Axiom or Definition must be
"parseable" into a composition of Syntax Axioms, and thus, will have
a derived Type code that matches one of the Syntax Axiom Type codes.
Usually this derived Type code is "wff
"
(by convention, "wff" is commonly used "in the logic biz" as an
acronym for "well-formed formula" and refers to a logical formula that may be evaluated as True or False.) For
example, in Theorem a1i
the $p
statement "a1i $p |- ( ps -> ph ) $.
" has a Formula with Type code "|-
" and Expression "( ps -> ph )
" which is parseable using Syntax Axiom wi, which has Type code "wff
". So, essentially, the a1i
Formula is saying in English, 'The wff, "( ps -> ph )
" is provable.'miu.mm
can be coded without a complete
set of Syntax Axioms. The problem with this idea is that Metamath
Theorems can be proven without Syntax Axioms, but essentially then, the
subject matter of the Theorems is not well
defined -- it is thus, just a sequence of symbols -- and so we may be
proving something but not be entirely sure what the statement is about.x = y
" as "vx cv vy cv wceq
", depending upon the needs of the theorem being proved while the mmj2 Proof Assistant was parsing the same sub-expression as "vx vy weq
". The mmj2 Proof Assistant By changing the definition of "weq
" from Axiom to Theorem, the conflict was resolved! Here is the old definition of "weq
" weq $a wff x = y $.
weq $p wff x = y $= vx cv vy cv wceq $.
weq
" in set.mm is now relegated to "syntactic sugar" that disppears internally -- every occurrence of "x = y
", or "A = B
" in Metamath proof derivation steps actually refers to class equality now, there is no distinct set equality operator. Analogous definitions are made for "member of" and other overloaded operator definitions.$a
,
which is the same statement used for logical axioms. This is part of
the beauty and elegance of Metamath, its "simplicity engineering". In
practice what it also means is that an expression's Syntax Tree -- the
output of the Grammatical Parser -- can be converted to the same RPN
format used by Metamath proofs -- and then the syntax RPN's can be
input into the Metamath Proof Verification algorithm, which will then
re-generate the original expression! In mmj2, in fact, the "VerifyParse,*
" RunParm uses this property to validate the output of the Grammatical Parser! When "VerifyParse,*
" is input, every Syntax Tree generated by the "Parse,*
"
RunParm command is converted to an RPN, fed into the ProofVerify
program, the output is compared to the original expression, and any
differences are reported (which would indicate a rather severe bug in
mmj2! -- so it would be wasteful to run "VerifyParse,*
" all the time, but if your computer is fast and you are a person who wears belt, suspenders and velcro to keep your trousers up, then go ahead :)