FOM: Re: Chaitin

[Harvey Friedman]

Reply to Raatikainen 11:12AM 3/28/01.

>On 27 Mar 01, at 20:28, 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.
>
>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 ?

Yes. It gives, or can be made to give, a low level computable total
function which takes any standard r.e. index of any consistent r.e. theory
with finitely many sorts which interprets EFA, and produces a c such that
for all n, K(n) > c is not provable in that theory, where the latter is
formlaized in terms of any interpretation of EFA into that theory.

>Friedman wrote:
>
>> SOME REVERSE MATH OF KOLMOGOROV COMPLEXITY
>>
>> Sigma-0-1 induction is sufficient to prove for all n, K(n) exists, and to
>> prove the existence of Kolmogorov random integers.
>>
>> What is the status over EFA of
>> i) for all n, K(n) exists;
>> ii) the function K is defined on every interval [0,n];
>> iii) the function K achieves a maximum value on every interval [0,n];
>> iv) there is a Kolmogorov random bit sequence of each length.
>
>(etc.)
>
>RE: This sounds very exciting - I just want to remark that it is
>interesting that although it is possible to formalize the basic
>recursion theory in HA (see e.g. Troelstra and van Dalen, Vol. 1, p.
>152-), it is *not* possible to prove i) "for all n, K(n) exists" in HA, for
>it requires the Least Number Principle (and thus classical logic)
>applied to  a Sigma-O-1 formula.

I'm not sure if you regard this paragraph as a proof that HA is
insufficient. In fact, HA is insufficient to prove any
of i) - iv). In fact, any formal system based on intuitionistic logic with
the following property is insufficient to prove any of i) - iv):

*) Suppose (forall n)(therexists m)(phi(n,m)) is provable. Then there is a
recursive function f such that (forall n)(phi(n,f(n)) is true.

In fact, all we need is *) for Pi-0-1 formulas phi with only the free
variables shown.

In particular, the following cannot be proved in such a system:

"for all k there exists n such that all programs for n have at least k symbols"