Metamath
 |
|
| Developer(s) | Norman Megill |
|---|---|
| Written in | ANSI C |
| Operating system | Linux, Windows, Mac OS |
| Type | Computer-assisted proof checking |
| License | GNU General Public License (Creative Commons Public Domain Dedication for databases) |
| Website | http://metamath.org |
A proof of the Metamath Proof Explorer
|
|
|
Type of site
|
Internet encyclopedia project |
|---|---|
| Headquarters | USA |
| Owner | Norman Megill |
| Created by | Norman Megill |
| Website | us.metamath.org/mpegif/mmset.html |
| Alexa rank |
 2,281,276 (April 2014[update]) |
| Commercial | No |
| Registration | No |
Metamath is a language for developing strictly formalized mathematical definitions and proofs accompanied by a proof checker for this language and a growing database of thousands of proved theorems covering conventional results in logic, set theory, number theory, group theory, algebra, analysis, and topology, as well as topics in Hilbert spaces and quantum logic.
While the large database of proved theorems follows conventional ZFC set theory, the Metamath language is a metalanguage, suitable for developing a wide variety of formal systems.
The set of symbols that can be used for constructing formulas is declared using $c and $v statements; for example:
The grammar for formulas is specified using a combination of $f and $a statements; for example:
Axioms and rules of inference are specified with $a statements along with ${ and $} for block scoping; for example:
The metamath program can convert statements to more conventional TeX notation; for example, the modus ponens axiom from set.mm:
Using one construct, $a statements, to capture syntactic rules, axiom schemas, and rules of inference provides a level of flexibility similar to higher order logical frameworks without a dependency on a complex type system.
Theorems (and derived rules of inference) are written with $p statements; for example:
Note the inclusion of the proof in the $p statement. It abbreviates the following detailed proof:
The "essential" form of the proof elides syntactic details, leaving a more conventional presentation:
Metamath has no specific logic embedded and can simply be regarded as a device to apply inference rules to formulas. Simplicity is the master concept in the design of Metamath: the language of Metamath, 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). This "substitution" is just the simple replacement of a variable with an expression and not the proper substitution described in works on predicate calculus.
...
Wikipedia