Gödel's Incompleteness proof Incompletely implemented

Gödel proved Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme the incompleteness of minimal logic combined with minimal arithmetic. He was careful to point out that every step in the proof is constructive. So one would assume that the whole process up to the unprovable theorem about numbers could be implemented. The original paper in fact has a point by point implementation in Gödels's own notation of primitive recursion. Porting this to Scheme seemed viable.

Gödel has a curious programming style, specially when it comes to performance. For example, after definition of Pr(n) as the n-th prime number, l(n) as the number of encoded numbers in n, and n Gl x as the n-th coded number in the number x, he defines the concatenation of terms x and y as

x * y =
ε z { z ≤ [Pr((l(x)+l(y)))]x+y & 
             (n) [n≤l(x) → n Gl z = n Gl x ] &
	         (n) [0 < n ≤ l(y) → (n+l(x)) Gl z = n Gl y ]}

which translates as :

To get the concatenation of x and y, find the first number z, starting from 1, such that z is smaller than the len(x) + len(y)-th prime taken to the (x+y)-th power, and such that for all n less than len(x) the n-th term in z is the n-th term in x, and such that for all n less than len(y), the (n+len(x))-th term in z is the n-th term in y

Remember that the n-th encoded term k in x is the factor (n-th prime)^k of x, so this algorithm will try an incredible number of wrong candidates before reaching a likely candidate.

While implementing Gödel's proof in a kind of Test Driven Development I had to stop at point 22 in the original paper, because from that point on even trivial tests will not finish before the sun burns out. For an explanation, see
end of code.

Wed, 25 Mar 2015
[/projects] permanent link