The number of the beast

by Michael Brunnbauer, 2014-04-22

This work is dedicated to Hans Hermes. If I had to forget all books I have read but one, I would choose to remember his book "Einführung in die mathematische Logik".

The proof of Gödel's first incompleteness theorem uses a self-referential formula that basically means "I am not provable". What is easily overlooked is that the short hand notation used in the proof is just that. The Gödel sentence cannot use non-elementary symbols because it has to be provable or unprovable by itself. All definitions have to be reduced to the elementary symbols of Peano arithmetic.

This is what I have tried - with partial success. I was able to generate the first stage with 19GB and estimate the final thing to have at least 740GB.

You can find the codebase to try it yourself on Github

In a nutshell

Numbers (Gödel-numbers) are assigned to symbols, formulae constructed from those symbols and proofs constructed from the formulae. The assignment allows to reconstruct the symbols, formulae and proofs from the numbers.

Functions are then defined that determine what numbers are valid formulae and proofs or that manipulate formulae. These functions are simple expressions or primitive recursive functions - which basically means that they can be calculated effectively e.g. they do not require unbounded loops/recursion when implemented as algorithm.

The Gödel sentence is constructed using:

A function isvalidprooffor(x,y), which is 1 if x is a valid proof for y, else 0.

A function number(x), which yields the Gödel-number of a term that yields the number x using 0 and the sucessor function.

A function subst_formula(f,v,t) which substitutes the free variable v in formula f with term t.

We first define the formula p:

p = for all x: not isvalidprooffor(x,subst_formula(y,[y],number(y))) = 1

[y] is a term that yields the Gödel-number of variable y.

p is the first stage I was able to generate with 19GB size (the formula, not its Gödel-number).

The Gödel sentence would then be: subst_formula([p],[y],number([p])), where [p] is a term yielding the Gödel-number of p.

G = subst_formula([p],[y],number([p]))

If we actually do the "subst_formula", we get:

g = for all x: not isvalidprooffor(x,subst_formula([p],[y],number([p]))) = 1

We can now see that g is equivalent to "for all x: not isvalidprooffor(x,[g]) = 1":

g <-> for all x: not isvalidprooffor(x,[g]) = 1

This allows to infer that g is unprovable and - assuming ω-consistency - that there is no proof for the negation of g.

Note that g does not follow from "there exists x such that: isvalidprooffor(x,[g]) = 1". The notion of syntactical inference uses the standard model of natural numbers but the mentioned formula is not limited in this way.

"a", not "the"

Of course, what I tried to generate is strictly a Gödel sentence, not the Gödel sentence because there are so many ways to do it. What follows are the technical details of my approach.

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. The arithmetization does not use prime numbers but powers ot two.

Gödelization scheme

Variables, terms, propositions, formulae, sequences of formulae and proofs are certain ASCII-strings interpreted as the numbers corresponding to their bitstream.

Definition of a formula

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)

Definition of sequences and proofs

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.

Arithmetization of syntactical inference

The notion of formulae, free variables, substitution, sequences of formulae and proofs are defined as primitive recursive functions using the symbols n0-n256, sc(x), ad(x,y) and mu(x,y) 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.

Definitions (informal, with comments)

The definitions start with n1-n256 representing the numbers 1-256.

The calculus

The sequent calculus (taken from Hans Hermes book mentioned above) 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 ...)

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

Types of functions

There are five types of functions (see functions.py):

Resolving a primitive recursive function call to a formula

f(x) for a primitive recursive function with f(0)=c and f(x+1)=g(f(x),x) is resolved to:

∃a∃m( rm(a,m*(0+1)+1)=c ∧ ∀i<x( g(rm(a,m*(i+1)+1),i)=rm(a,m*(i+1+1)+1) ) )

Informally: There exists a,m such that the remainder of a divided by m*(i+1)+1 is f(i) for all i <= x (the sequence of values of the function up to f(x) is coded into a,m).

f(x) is then rm(a,m*(x+1)+1).

rm(a,b) is resolved to: ∃c∃d( a=(b*c)+d ∧ d<b )

rm(a,b) is then d.

a<b is resolved to: ∃i a+(i+1)=b

If you find any error in my reasoning, definitions or the code, please let me know.

Corrections since publication