-
Notifications
You must be signed in to change notification settings - Fork 1
/
README
222 lines (153 loc) · 6.51 KB
/
README
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
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
generategoedelsentence.py will generate the first stage of the Gödel sentence,
which is 19GB big. You will need more memory than this to run it.
If you have terabytes of memory and plenty of time, you may be able to
generate the Gödel sentence itself, which - according to my estimate - should
be at least 740GB big.
The codebase enables creation of functions based on expressions, primitive
recursion and more unrestricted forms of recursion that can be reduced to
primitive recursion. It is possible to automatically print the primitive
recursive definitions, compute with the functions and to reduce a term
composed of these functions to an elementary formula consisting only of 0,
the successor, addition and multiplication.
The latter is needed for the Gödel sentence because it has to be provable
or unprovable by itself and therefore should only contain elementary symbols.
Author: Michael Brunnbauer, [email protected]
See http://www.brunni.de/goedel/the_number_of_the_beast.html for an article
about this work.
The primitive recursive functions isvalidprooffor(x,y), subst_formula(x,y,z)
and number(x) used in the Gödel sentence are defined using ASCII-based
Gödelization and a first order logic sequent calculus augmented with the
6 first order axioms of Peano arithmetic and the induction scheme.
See http://www.brunni.de/goedel/definitions.txt for the complete printed
definition generated by printdefinitions.py.
The sequent calculus and the proof examples are from the book "Einführung
in die mathematische Logik" by Hans Hermes, published by B.G. Teubner
Stuttgart 1991.
Variables, terms, propositions, formulae, sequences of formulae and proofs
are certain ASCII-strings interpreted as the numbers corresponding to their
bitstream.
Definitions:
namelc: Names for variables and functions are lower case strings consisting of
a-z,0-9 and _ starting with a-z.
nameuc: Names for predicates are upper case strings consisting of
A-Z,0-9 and _ starting with A-Z.
The following definitions use BNF grammar:
termlist:
term
termlist , term
term:
namelc
namelc ( termlist )
proposition:
nameuc ( termlist )
equation:
term = term
formula:
proposition
equation
~ formula
( formula & formula )
! namelc : formula
(proposition,equation,negation,conjunction,generalization)
The usual definitions of the terms "variable x is free in formula f" and
"formula b is a substitution of term t for variable x in formula a" apply
(see functions_freevariable.py and functions_subst.py for details).
A sequence of formulae is a concatenation of formulae delimited by ; and
ending with ;. The last formula in a sequence is meant to be implied by the
preceding ones.
A proof is a concatenation of sequences of formulae delimited by \n and
ending with \n. A valid proof is a proof where every line can be generated by
application of a rule of the calculus on zero, one or two of the preceding
lines.
The sequent calculus has the following rules. A and B are formulae, t is a
term, x is a variable, ... and --- are sequences of zero or more formulae.
1) A formula implies itself:
A A
2) Introduction of conjunction
... A
--- B
... --- (A&B)
3) Removal of conjunction1
... (A&B)
... A
4) Removal of conjunction2
... (A&B)
... B
5) Exhaustion
... A B
--- ~A B
... --- B
6) Ex contradictione quodlibet
... A
--- ~A
... --- B
7) Removal of generalization
... !x:A
... A
8) Introduction of generalization
... A
... !x:A (if x is not free in ...)
9) Substitution
... A
--- B (if ... B is a substitution of t for x in ... A)
10) Tautological equation
t=t
11) Substitution with assertion of identity
... A
... x=t B (if B is a substitution of t for x in A)
The sequences ..., --- or ... --- in the resulting sequence only have to
contain the same formulae as ..., --- or ... ---. It is allowed to permutate
and to introduce or remove repetitions - except in rule 9. An additional
rule allows to permutate to get the required order for rule 5:
12) Permutation
... A
--- A (Where --- contains the same formulae as ...)
We use the symbols n0-n256, sc(), ad() and mu() for the numbers 0-256, the
successor function, addition and multiplication. The symbols n1-n256 can
be replaced with repeated application of sc() on n0 when needed.
These are the additional rules for Peano arithmetic:
13) You can write any of these formulae as sequence with empty premise:
!x:~n0=sc(x)
!x:!y:~(sc(x)=sc(y)&~x=y)
!x:ad(x,n0)=x
!x:!y:ad(x,sc(y))=sc(ad(x,y))
!x:mu(x,n0)=n0
!x:!y:mu(x,sc(y))=ad(mu(x,y),x)
14) Induction scheme. It is allowed to write a sequence:
--- (A&!x:~(B&~C)) ; --- !x:B
where:
n0 is free in A
B = subst_formula(A,n0,x)
C = subst_formula(A,n0,sc(x))
--- is empty or a list of generalizations not containing variable x or n0
You can find example proofs in the subdirectory proofs.
There are five types of functions (see functions.py):
-Basic functions defined by an expression
-Primitive recursive functions defined by the value for 0 and the value for
n+1 based on the value for n
-Argmin-functions returning the smallest number within a range 0-max for
which a function does not return 0 - otherwise 0. These are defined using
primitive recursive functions.
-"Recursive relations" returning 0 or 1 defined by the value for 0 and the
value for some number based on values for smaller numbers. These are defined
using a primitive recursive function h(x) so that f(x) = bit x of h(x).
In other words: h(x) codes all results of f(x) from 0-x using powers of two.
Actual computation uses unrestricted recursion because computing h(x) is
not feasible in practice.
-"Recursive functions" returning arbitrary values defined by the value for 0
and the value for some number based on values for smaller numbers. These are
defined analogous to "Recursive relations" using a primitive recursive
function h(x) so that f(x) = bit a-b of h(x). a and b are determined with a
primitive recursive function bitstart so that a = bitstart(x) and b =
bitstart(x+1)-1.
All definitions use powers to 2 to code and extract information instead of
prime numbers.
Use printdefinitions.py to print all definitions.
Use checkproof.py <file> to check a proof in ASCII-file <file> for vadility
using computation on its Gödel number.
Use testsuite.py to run a testsuite.
Use elementaryformula.py to convert a term into a almost elementary formula
using only n0-n256, sc(), ad() and mu() - almost because the symbols
n1-n256 are not elementary but can easily be replaced with sc() and n0.
Use generategoedelsentence.py to generate the first stage of the Gödel
sentence.