Q. What are Metamath Syntax, Axioms and Definitions?

A.

`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. Q. What are Syntax Axioms?

A. Syntax Axioms are the user-created Metamath axiom statements that define the "things", the subject matter, such as

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).For example, in

`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 "`|-`

". Q. What is the difference between Syntax Axioms, Named Typed-Constant Axioms, Type Conversion Axioms, and Nulls-Permitted Axioms?

A. Named Typed Constant Axioms, Type Conversion Axioms and Nulls-Permitted are a subset of "Syntax Axioms", per se. However, they may be viewed as idioms, or commonly used constructions that are useful and distinctive enough to warrant special treatment in processing, especially grammatical parsing. See ExampleMetamathDatabase.html for examples.

Named Typed String Axioms are perhaps not useful and have not been seen in "real" Metamath databases, but are named herein for the sake of consistency as part of the class of Syntax Axioms that have no Variables, consisting solely of Constants:

`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 { } $.` |

Note: It is allowed to use a Constant in a Syntax Axiom that is named elsewhere by a Named Typed-Constant Axiom. An example of this in set.mm is the Constant "/". Consider valid usage:

$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 $.

In "wsbc" and "wsb" the Constant "/" is just punctuation, an actual Constant, but in "cdiv" the Constant "/" is assigned a name and a type: "cdiv" and "class". This means that the Constant "/" can be used anyplace that a class variable is expected, but nevertheless, in "wsbc" and "wsb" it is not a class, it is just a slash mark! That can be confusing, I think, and for the sake of clarity it is recommended that Constants named by Named Typed Constant Axioms not be used elsewhere in any other Syntax Axioms, at all.

ExampleMetamathDatabase.html

ExampleMetamathGrammar.html

Q. How do"Types" relate to Axioms, Theorems and Hypotheses?A. Metamath formulas are required to be at least one symbol in length. The first symbol of a Formula must be a Constant -- which is the Type (code) of the formula. The Type code provides a context for the remaining symbols in the formula and says, "These symbols make up a XXX" where "XXX" is the Type code. For example, in

`wn $a wff -. ph $. `

the first symbol of the formula is "

`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`

".
Note: hereafter I refer to a statement's Formula's symbols that follow the Type code as the "Expression" and use the word "Formula" to refer to the entire symbol sequence including the type code. Thus, for statement

`wn`

- "
`wff -. ph`

" is the formula, and - "
`-. ph`

" is the expression in the`wn`

statement.

In Metamath, the only way that new formulas can be deduced or generated from existing formulas is by substitution of new Expressions for existing Variables. For example:

- given formula "
`wff -. ph`

" - substitute "
`( ph -> ps )`

" into the formula, replacing variable`ph`

- to create the new formula "
`wff -. ( ph -> ps )`

".

`wff`

variable can only be replaced by a `wff`

expression.)Thus, a Theorem with Type code "|-", for example, can only be deduced from Logical Axioms, Definitions and Logical Hypotheses that have a matching "|-" Type code. No possible substitution can generate a Theorem's Formula from a Syntax Axiom's Formula, assuming the Type codes are different.

Note: Metamath does not prohibit Syntax Axioms from having the same Type code used on Theorems, Logical Axioms, etc. But this usage is not typically seen. Suppose the user has defined a Logical statement type code "

`|-`

". 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.)Q. What Are "Derived Type Codes"?

A. In standard Metamath practice (

`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.'Metamath does not require that logical formulas be parseable into Syntax Axioms and thus have deriveable Type codes. In fact, the sample Metamath database

`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.Q. What Are "Syntax Proofs"?

A. A "Syntax Proof" is a bit of Metamath trickery that allows formulas to be written with operator overloading without using operator overloading in Metamath proofs. They were invented by Norman Megill as a way to eliminate any possible grammatical ambiguities within set.mm after it was discovered that the Metamath.exe Proof Assistant was parsing certain occurrences of "

`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 $.`

And the new definition:

` weq $p wff x = y $= vx cv vy cv wceq $.`

Thus, "

`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.Note: this may seem confusing, especially if you are new to Metamath. The reason that this works at all is that in Metamath the syntax of a .mm database/file is built using the axiom declaration statement

`$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 :)