The Shœstring Foundation Weblog About The Shœstring Foundation Weblog, Miscellaneous Byproducts Matthias Bauer `bauerm (at) shoestringfoundation · org ` reop pubkey Vignettes by George Herriman and a small program Subscribe to a syndicated feed of my weblog, brought to you by the wonders of RSS. Wed, 25 Mar 2015 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.