Developer(s) | Norman Megill |
---|---|
Written in | ANSI C |
Operating system | Linux, Windows, macOS |
Type | Computer-assisted proof checking |
License | GNU General Public License (Creative CommonsPublic Domain Dedication for databases) |
Website | metamath.org |
$c
(constant symbols)and $v
(variable symbols) statements; for example:$f
(floating (variable-type)hypotheses) and $a
(axiomatic assertion) statements; for example:$a
statementsalong with ${
and $}
for block scoping andoptional $e
(essential hypotheses) statements; for example:$a
statements, to capture syntactic rules, axiom schemas, and rules of inference is intended to provide a level of flexibility similar to higher order logical frameworks without a dependency on a complex type system.$p
statements;for example:$p
statement. It abbreviatesthe following detailed proof:2p2e4
in the Metamath Proof Explorer (set.mm) are depicted left. Let's explain how Metamath uses its substitution algorithm to check that step 2 is the logical consequence of step 1 when you use the theorem opreq2i
. Step 2 states that ( 2 + 2 ) = ( 2 + ( 1 + 1 ) ). It is the conclusion of the theorem opreq2i
. The theorem opreq2i
states that if A = B, then (C F A) = (C F B). This theorem would never appear under this cryptic form in a textbook but its literate formulation is banal: when two quantities are equal, one can replace one by the other in an operation. To check the proof Metamath attempts to unify (C F A) = (C F B) with ( 2 + 2 ) = ( 2 + ( 1 + 1 ) ). There is only one way to do so: unifying C with 2, F with +, A with 2 and B with ( 1 + 1 ). So now Metamath uses the premise of opreq2i
. This premise states that A = B. As a consequence of its previous computation, Metamath knows that A should be substituted by 2 and B by ( 1 + 1 ). The premise A = B becomes 2=( 1 + 1 ) and thus step 1 is therefore generated. In its turn step 1 is unified with df-2
. df-2
is the definition of the number 2
and states that 2 = ( 1 + 1 )
. Here the unification is simply a matter of constants and is straightforward (no problem of variables to substitute). So the verification is finished and these two steps of the proof of 2p2e4
are correct.class
thus Metamath has to check that ( 2 + 2 ) is also typed class
.A proof of the Metamath Proof Explorer | |
Online encyclopedia | |
Headquarters | USA |
---|---|
Owner | Norman Megill |
Created by | Norman Megill |
URL | us.metamath.org/mpeuni/mmset.html |
Commercial | No |
Registration | No |