FOM: RE: Chaitin

[Harvey Friedman]

Reply to Marandjian 9:13AM 3/30/01.

>On 27 Mar 01, Harvey Friedman wrote:
>
>> THEOREM. Let T be a consistent recursively axiomatizable extension of EFA
>> (exponential function arithmetic), possibly with additional sorts. There
>is
>> a constant c such that for all n, K(n) > c is not provable in T.

>It is possible to prove more strong proposition that is true not only for
>proofs in the theories under discussion but also for any algorithmic method
>of generating true assertions of the form K(n)>c and answers  Panu
>Raatikainen's
>question:
>
>THEOREM. There exists such a total recursive function f that
>for any recursively enumerable set W_m of pairs <a,b> such
>that K(a) > b, for any x no pair <x,f(m)> belongs to W_m.
>
>Hence, if W_m is the set of pairs <a,b> corresponding to provable assertions
>
>of the form K(a) > b in a consistent theory T enabling one to enumerate
>recursively such pairs, then thisi theorem gives the constant C under
>question.
>
>This theorem is an evident consequence of the result
>available in English from:
>
>H.B.Marandjian, (misspelled as G. B. Marand\v{z}jan)
>On algorithms of minimal complexity,
>Soviet. Math. Docl., 1973, v.14, No.6,1797--1799.
>
Your theorem is better than mine. It also shows how valuable the FOM e-mail
list is.

One point of clarification. You do need that if T proves K(a) > b then K(a)
> b is true, and that appears to be a form of soundness. However K(a) > b
is always a Pi-0-1 sentence, and so it is just consistency, and no more.

To complete the circle, here is an easy derivation of your theorem from
mine, in the effective form that I wrote about on 2:57AM 3/30.01.

Let f be the effectivizer for my Theorem above. Let W_m be a set of pairs
<a,b> such that K(a) > b. Let T be EFA plus the set of sentences K(a) > b
for <a,b> in W_m. Then T is consistent since it is true. Hence for all n,
K(n) > c is not provable in T. Hence for all n, K(n) > c is not in W_m.
Here c is effectively obtained from the index of T, and hence effectively
obtained from the index m.

What is the result in your paper of which your Theorem is an evident
consequence? Perhaps this might tell us why your Theorem was perhaps not
more widely known to people studying Chaitin?