 The Metamath language design is focused on simplicity; the language, employed to state the definitions, axioms, inference rules and theorems is only composed of a handful of keywords, and all the proofs are checked using one simple algorithm based on the substitution of variables (with optional provisos for what variables must remain distinct after a substitution is made).The set of symbols that can be used for constructing formulas is declared using codice_1
and codice_2 (variable symbols) statements; for example