The Shœstring Foundation Weblog

The Shœstring Foundation Weblog, Miscellaneous Byproducts

Matthias Bauer
bauerm (at) shoestringfoundation · org
reop pubkey
Vignettes by George Herriman

Subscribe to a syndicated feed of my weblog, brought to you by the wonders of RSS.

Blosxom Logo

Wed, 25 Mar 2015

Gödel's Incompleteness proof Incompletely implemented

Gödel proved 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.

[/projects] permanent link