based on ExampleMetamathDatabase.html
Rule |
Left
|
→ |
Right Side
|
Label
|
Parameter Transformations
|
1 |
wff
|
→ |
-. wff
|
wn
|
[ ]
|
2 |
|
|
|
( wff -> wff )
|
wi
|
[ , ]
|
3 |
|
|
|
( wff <-> wff )
|
wb
|
[ , ]
|
4 |
|
|
|
set = set
|
weq
|
[ , ]
|
5 |
|
|
|
class = class
|
wceq
|
[ , ]
|
6 |
|
|
|
class = set
|
wceq
|
[ , cv ]
|
7 |
|
|
|
set = class
|
wceq
|
[ cv , ]
|
8 |
set
|
→ |
|
|
|
9 |
|
| |
|
|
|
10 |
class
|
→ |
(/)
|
c0
|
n/a
|
11 |
| |
THIS HAS FOUR CONSTANTS |
cString |
n/a |
|
12 |
|
| |
suc class
|
csuc
|
[ ]
|
13 |
|
| |
suc set
|
csuc
|
[ cv ]
|
14 |
|
|
|
sup ( class , class , class )
|
csup
|
[ , , ]
|
15 |
|
|
|
sup ( class , class , set )
|
csup
|
[ , , cv ] |
16 |
|
|
|
sup ( class , set , class )
|
csup
|
[ , cv , ]
|
17 |
|
|
|
sup ( class , set , set )
|
csup
|
[ , cv , cv ]
|
18 |
|
|
|
sup ( set , class , class )
|
csup
|
[ cv , , ]
|
19 |
|
|
|
sup ( set , class , set )
|
csup
|
[ cv , , cv ]
|
20 |
| |
| sup ( set , set , class )
| csup
| [ cv , cv , ]
|
21 |
| |
| sup ( set , set , set )
| csup
| [ cv , cv , cv ]
|
22 |
|||||
23 |
|||||
24 |
|||||
25 |
|||||
26 |
|||||
27 |
set.mm with minor changes)$( ---------------------------------------------------------------------------------------
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
$)
cv $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 and Type Conversion 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 $)
c0 $a class (/) $. $( Named-Typed Constant Axiom :
Constant "(/)" has type Class;
"(/)" stands for the Empty Set;
label "c0" can
be used in
proofs
$)
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 $)
$( ---------------------------------------------------------------------------------------
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 $)
$}