Tokens#

A database is tokens separated by white space, drawn from the 94 printable ASCII characters. Three kinds:

• keywords, which all begin with $
• labels, which name statements
• math symbols, anything else

Metamath book, section 4.1

The keywords#

${ $}  $c $v  $f $e $d  $a $p  $. $=  $( $) $[ $]

The last four handle comments and file inclusion.

Metamath book, section 4.1

Statements: declaring#

• $c declares constants
• $v declares variables
• $f and $e are hypotheses
• $d restricts substitution

Metamath book, section 4.1

Statements: asserting#

• $a asserts an axiom
• $p asserts a theorem, and carries its proof after $=
• ${ $} bounds a block, which limits how long a declaration stays active

Metamath book, section 4.1

The book#

• Norman Megill, with extensive revisions by David A. Wheeler
• 248 pages
• Source and errata on GitHub, under CC0
• A German translation

Metamath book (PDF)

A condensed introduction#

Ivan Kuckir’s opens: “Official Metamath description has 211 pages. This is a “shrinked” version”.

It reads Metamath as a grammar: $c declares terminal symbols, $v nonterminals.

Introduction to Metamath · Other Topics

Grammar one: MM.g4#

The Antlr4 grammar behind the gramm verifier, on one screen:

• a database is stat* EOF
• a label is [A-Za-z0-9._-]+
• a math word is any run of characters without white space or $

MM.g4

Grammar two, and what a grammar is not#

A tree-sitter grammar parses a database into a syntax tree from Python.

Neither says whether a proof is right. A grammar only tokenises and parses.

$j#

“a way to include information in metamath proof files which are not needed for verifying, but which are useful for other tools”

A kind of comment (book, section 4.4.3), so a verifier may skip them.

Metamath $j commands

Before Wednesday’s lab#

1. Download miu.mm and peano.mm
2. Have section 4.1 of the book open
3. Bring metamath-exe from week 1

Read before next week#

• Metamath book, section 4.1: the four pages themselves, twice before Wednesday
• Introduction to Metamath: the same material as a grammar, in a few screens
• MM.g4: the surface syntax at its shortest