BASICS OF SYNTAX AXIOMS and TYPES

(see also: SyntaxAxiomRulesAndConventions.html)

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
Length
 Name of
Syntax Axiom
Subset
 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

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:
The key point here is that only the Variables in an existing formula can be replaced with new Expressions; the Type code in an existing formula can never be changed, no matter what.  As substitutions are performed by Metamath (in the Proof Engine), strict Type code checking is done. A substitution Expression must have the same Type code as the Variable it is replacing. (I.E. a 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 :)