_{1}, ..., a

_{n}> is coded as: 2

^{a1}× ... ×p

_{n}

^{an}, where p

_{n}is the n

^{th}prime. The 'star function' is then defined as follows:

x * y = μz≤Pr[l(x) + l(y)]Here, l(x) is the length of the sequence x; n Gl x is the n^{x+y}{∀n≤l(x)(n Gl z = n Gl x) &

∀n≤l(y)(0<n → (n + l(x)) Gl z = n Gl y)}

^{th}element of that sequence. So the definition says that x * y is the least number coding a sequence that agrees with x on its first l(x) elements and agrees with y on the next l(y) elements. Of course, there is such a number (and, actually, given how "Gl" works, there are infinitely many). The bound is needed to guarantee that * is primitive recursive.

The question, though, is how the bound is supposed to work. Gödel does not often discuss his bounds, which tend to be pretty loose, but he does explain one of them in footnote 35. And if one follows the sort of reasoning Gödel uses there, then it is difficult to see how to get the bound in the above.

I asked a question about this on the Foundations of Mathematics mailing list, and Alasdair Urquhart took the bait and replied with an elegant proof showing why Gödel's bound works. I thought I'd record a version of it here, in case anyone else has a similar question.

First, we show, by a straightforward induction on n, that 2

^{a1}× ... ×p

_{n}

^{an}≤ p

_{n}

^{a1 + ... + an}.

Now let <a

_{1}, ..., a

_{n}> and <b

_{1}, ..., b

_{m}> be two sequences. The code of their concatenation is:

2Moreover,^{a1}× ... ×p_{n}^{an}× p_{n+1}^{b1}× ... × p_{n+m}^{bm}≤ p_{n+m}^{a1 + ... + an + b1 + ... + bm}

aand similarly for the other sequence. (Note that the last inequality depends upon the fact that none of the a_{1}+ ... + a_{n}≤ 2^{a1}+ ... + p_{n}^{an}≤ 2^{a1}× ... × p_{n}^{an}= x

_{i}= 0, but Gödel's coding of sequences only works for positive integers.) So

awhich gives Gödel's bound._{1}+ ... + a_{n}+ a_{n+1}+ ... + a_{n+m}≤ x + y

## No comments:

## Post a Comment

Comments welcome, but they are expected to be civil.

Please don't bother spamming me. I'm only going to delete it.