ExampleMetamathDatabase.html
see ExampleMetamathGrammar.html
EXAMPLE Metamath database (based on set.mm with minor changes)
Note the statement categories:
1) Declarations and Variable Hypotheses
2) Syntax Axioms
3) Logical Axioms and Definitions
4) Theorems and Logical Hypotheses
$( ---------------------------------------------------------------------------------------
DECLARATIONS and VARIABLE HYPOTHESES
--------------------------------------------------------------------------------------- $)
$( Declarations
for Constant and Variable Symbols in the Metamath
database
$)
$c
wff
$.
$( Constant, identifies type "wff" -- well-formed
formulas $)
$c set $.
$( Constant, identifies type "set" -- mathematical sets
$)
$c class $.
$( Constant, identifies type "class" -- mathematical classes $)
$c |- $.
$( Constant, identifies type "|-" -- true/provable statements $)
$c (
$.
$( Constant, used as punctuation, aka "left
parentheses" $)
$c ) $.
$( Constant, used as punctuation, aka "right
parentheses" $)
$c -> $.
$( Constant, used as logical operator, aka "not"
$)
$c -. $.
$( Constant, used as logical operator, aka "implies"
$)
$C <->
$.
$( Constant, used as logical operator, aka "if and only if"
$)
$v ph ps ch $. $(
Variables: phi, psi and chi
$)
$v x y z
$. $( Variables:
x, y, and
z
$)
$v A B C
$. $( Variables:
A, B, and
C
$)
$( Variable Hypotheseses -- aka "Floating Hypotheses" -- assign a Type to a Variable $)
wph $f wff
ph $. $( Variable
ph has Type
wff
$)
wps $f
wff ps
$. $( Variable ps has
Type
wff
$)
wch $f
wff ch
$. $( Variable ch has
Type
wff
$)
vx $f
set x
$. $( Variable x has
Type set
$)
vy $f
set y
$. $( Variable y has
Type set
$)
vz $f
set z
$. $( Variable z has
Type set
$)
cA $f
class A $.
$( Variable A has Type
class
$)
cB $f class
B $. $(
Variable B has Type class
$)
cC $f
class C $.
$( Variable C has Type class
$)
$( ---------------------------------------------------------------------------------------
SYNTAX AXIOMS: Expression Axioms, Named-Typed Constant Axioms,
Named Typed String Axioms, Type Conversion Axioms and
Nulls-Permitted Axioms
--------------------------------------------------------------------------------------- $)
$( Syntax Axioms
$)
wn $a wff -. ph
$. $(
Expression Axiom "-. ph" has type wff $)
wi $a wff ( ph -> ps ) $. $( Expression Axiom "( ph -> ps )" has Type wff $)
wb $a wff ( ph <-> ps ) $. $( Expression Axiom "( ph <-> ps )" has Type wff $)
weq $a wff x = y $. $( Expression Axiom "x = y" has Type wff $)
wceq $a wff A = B $. $( Expression Axiom "A = B" has Type wff $)
csuc $a class suc class A $. $( Expression Axiom "suc class A" has Type class $)
csup $a class sup ( A , B , C ) $. $( Expression Axiom "sup ( A , B , C )" has Type class $)
c0 $a class (/) $. $( Named Typed Constant Axiom :
Constant "(/)" has type Class;
"(/)" stands for the Empty Set;
label "c0" can
be used in
proofs
$)
cString
$a class THIS HAS FOUR CONSTANTS $.
$( Named Typed String Axiom :
- Sequence of Constants "THIS HAS FOUR CONSTANTS"
has type class;
- Have never seen this used, but it is simply a
Syntax Axiom with no Variables, like Named Typed
Constant Axioms and Nulls Permitted Axioms.
cv $a class x $. $( Type Conversion Axiom: every set is a class;
Literally means
"Every set, x, is a class";
label "cv" can
be used in proofs for Type Conversion $)
$( negative, no nulls for class! $)
$( Nulls-Permitted Axiom: nulls permitted for Type class? $)
$( ---------------------------------------------------------------------------------------
LOGICAL AXIOMS and DEFINITIONS
--------------------------------------------------------------------------------------- $)
$( Logical Axioms
$)
ax-1 $a |- ( ph
->
$( Logical Axiom, label = "ax-1", type = "|-" $)
( ps
-> ph ) )
$.
ax-2 $a
|- ( ( ph -> ( ps -> ch ) ) -> $( Logical Axiom, label = "ax-2", type = "|-" $)
( ( ph -> ps ) -> ( ph -> ch ) ) ) $.
ax-3 $a
|- ( ( -. ph -> -. ps ) -> $( Logical Axiom, label = "ax-3", type = "|-" $)
( ps -> ph ) ) $.
${
$( Logical Axiom, label = "ax-mp", type = "|-" $)
min $e |- ph $.
maj $e |- ( ph -> ps ) $.
ax-mp $a |- ps $.
$}
df-bi $a |- -. ( ( ( ph <-> ps ) -> $( Definition, label = "df-bi", type = "|-" $)
-. ( ( ph -> ps ) -> -. ( ps -> ph ) ) )
->
-. (
-. ( ( ph -> ps ) -> -. ( ps -> ph ) ) ->
( ph <-> ps ) ) ) $.
$( ---------------------------------------------------------------------------------------
THEOREMS and LOGICAL HYPOTHESES
--------------------------------------------------------------------------------------- $)
$(
Theorems
$)
${
a1i.1 $e |- ph
$.
$( Logical hypothesis, label = "a1i.1, type = "|-" $)
a1i $p |- ( ps -> ph ) $= $( Theorem (aka Provable Assertion)
label = "a1i", Type = "|-"
$)
wph wps wph wi a1i.1 wph wps ax-1 ax-mp $. $( Proof in
Reverse Polish Notation format $)
$}