FOM: RE: Chaitin

[Hrant Marandjian]

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.

On 28 Mar 01,  Raatikainen Panu A K wrote:

> RE: OK, I surrender;  I can only say that the standard proofs of 
> Chaitin's theorem have made some soundness assumptions. (I 
> don't know if I really followed Harvey's ingenious proof - I'll have to 
> reflect it for some time. But I have no reason to doubt it.)
> - one question: does this proof provide an effective upper bound for 
> c ? 


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.


Hrant B.Marandjian
Prof.,
Research Dept.
HPL Armenia
Komitas ave. 49/3 suite 900
Yerevan 375051
Republic of Armenia
e-mail:  hrant at arm.hpl.com