-
Notifications
You must be signed in to change notification settings - Fork 88
/
miu.mm
144 lines (114 loc) · 5.42 KB
/
miu.mm
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
$( This is the Metamath database miu.mm. $)
$( Metamath is a formal language and associated computer program for
archiving, verifying, and studying mathematical proofs, created by Norman
Dwight Megill (1950--2021). For more information, visit
https://us.metamath.org and
https://github.com/metamath/set.mm, and feel free to ask questions at
https://groups.google.com/g/metamath. $)
$( The database miu.mm was created by Norman Megill. $)
$( !
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
Metamath source file for Hofstadter's MIU system
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
~~ PUBLIC DOMAIN ~~
This work is waived of all rights, including copyright, according to the CC0
Public Domain Dedication. https://creativecommons.org/publicdomain/zero/1.0/
Norman Megill - https://us.metamath.org
$)
$(
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
The MIU-system: A simple formal system
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
Note: This formal system is unusual in that it allows empty wffs. To work
with a proof, you must type "MM> SET EMPTY_SUBSTITUTION ON" before using the
PROVE command. By default this is OFF in order to reduce the number of
ambiguous unification possibilities that have to be selected during the
construction of a proof.
Hofstadter's MIU-system is a simple example of a formal system that
illustrates some concepts of Metamath. See
Douglas R. Hofstadter,
"G\"{o}del, Escher, Bach: An Eternal Golden Braid"
(Vintage Books, New York, 1979), pp. 33ff.
for a description of the MIU-system.
The system has three constant symbols, M, I, and U. The sole axiom of the
system is MI. There are four rules:
Rule I: If you possess a string whose last letter is I, you can add
append a U at the end.
Rule II: Suppose you have Mx. Then you may add Mxx to your collection.
Rule III: If III occurs in one of the strings in your collection, you may
make a new string with U in place of III.
Rule IV: If UU occurs inside one of your strings, you can drop it.
Note: The following comment applied to an old version of the Metamath spec
that didn't require $f (variable type) hypotheses for variables and is no
longer applicable. The current spec was made stricter primarily to reduce
the likelihood of inconsistent toy axiom systems, effectively requiring the
concept of an "MIU wff" anyway. However, I am keeping the comment for
historical reasons, if only to point out an intrinsic difference in Rules III
and IV that might have relevance to other proof systems.
Old comment, obsolete: Unfortunately, Rules III and IV do not have unique
results: strings could have more than one occurrence of III or UU. This
requires that we introduce the concept of an "MIU well-formed formula" or
wff, which allows us to construct unique symbol sequences to which Rules III
and IV can be applied.
Under the old Metamath spec, the problem this caused was that without the
construction of specific wffs to substitute for their variables, Rules III
and IV would sometimes not have unique unifications (as required by the spec)
during a proof, making proofs more difficult or even impossible.
$)
$( First, we declare the constant symbols of the language. Note that we need
two symbols to distinguish the assertion that a sequence is a wff from the
assertion that it is a theorem; we have arbitrarily chosen "wff" and
"|-". $)
$c M I U |- wff $.
$( Next, we declare some variables. $)
$v x y $.
$( Throughout our theory, we shall assume that these variables represent
wffs. $)
wx $f wff x $.
wy $f wff y $.
$( Define MIU-wffs. We allow the empty sequence to be a wff. $)
$( The empty sequence is a wff. $)
we $a wff $.
$( "M" after any wff is a wff. $)
wM $a wff x M $.
$( "I" after any wff is a wff. $)
wI $a wff x I $.
$( "U" after any wff is a wff. $)
wU $a wff x U $.
$( If "x" and "y" are wffs, so is "x y". This allows the conclusion of Rule
IV to be provable as a wff before substitutions into it, for those parsers
requiring it. (Added per suggestion of Mel O'Cat, 4-Dec-2004.) $)
wxy $a wff x y $.
$( Assert the axiom. $)
ax $a |- M I $.
$( Assert the rules. $)
${
Ia $e |- x I $.
$( Given any theorem ending with "I", it remains a theorem if "U" is added
after it. (We distinguish the label ~ I_ from the math symbol ` I ` to
conform to the 24-Jun-2006 Metamath spec change.) $)
I_ $a |- x I U $.
$}
${
IIa $e |- M x $.
$( Given any theorem starting with "M", it remains a theorem if the part
after the "M" is added again after it. $)
II $a |- M x x $.
$}
${
IIIa $e |- x I I I y $.
$( Given any theorem with "III" in the middle, it remains a theorem if the
"III" is replaced with "U". $)
III $a |- x U y $.
$}
${
IVa $e |- x U U y $.
$( Given any theorem with "UU" in the middle, it remains a theorem if the
"UU" is deleted. $)
IV $a |- x y $.
$}
$( Now we prove the theorem MUIIU. You may be interested in comparing this
proof with that of Hofstadter (pp. 35--36). $)
theorem1 $p |- M U I I U $=
we wM wU wI we wI wU we wU wI wU we wM we wI wU we wM wI wI wI we wI wI we
wI ax II II I_ III II IV $.