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.