FOM: Re: Chaitin

[Harvey Friedman]

Reply to Raatikainen 3/27/01 12:58PM.

Raatikainen wrote

>> >a) Chaitin 1974 (mentioned by Charlie Silver).
>> >	For every formal system F, there is a finite constant c such
>> >	that F cannot prove any true statement of the form K(n) > c
>> >	(even thought there are infinitely many n for which this is true)
>> >	- here K(x) is the Kolmogorov complexity of x

Friedman wrote

>> I think that more is true:
>>
>> For every consistent reasonable formal system F, there is a finite constant
>> c such that F cannot prove any sentence of the form K(n) > c.

Raatikainen wrote

>RE: I think that both your formulation and mine are slightly inexact,
>namely, the proof of Chaitin's result actually requires that F proves
>a sentence of the form "K(n) > m" only it is true - that is, we need
>some amount of soundness and not just consistency (my wording
>was even worse here)  - or perhaps you meant just this by
>"reasonable" ...

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.

This follows immediately from

LEMMA. There is a Sigma-0-1 formula A(n,m) such that
i) T proves not(A(n,0) and A(n,1));
ii) for any infinite sequence x_0,x_1,... from {0,1}, T + {A(n,x_n): n >=
0} is consistent.

Proof: By self reference, we can find A such that the following two
statements are provable in T:

A(n,0) if and only if there is an inconsistency proof in some T +
A(0,i_0),A(1,i_1),...,A(n-1,i_n-1),A(n,0) which has lower Godel number than
any inconsistency proof in any T +
A(0,j_0),A(1,j_1),...,A(n-1,j_n-1),A(n,1). Here the i's and j's are taken
from {0,1}.

A(n,1) if and only if there is an inconsistency proof in some T +
A(0,i_0),A(1,i_1),...,A(n-1,i_n-1),A(n,1) which has lower Godel number than
any inconsistency proof in any T +
A(0,j_0),A(1,j_1),...,A(n-1,j_n-1),A(n,0). Here the i's and j's are taken
from {0,1}.

One proves by induction on n that for any sequence x_0,...,x_n from {0,1},
T + {A(n,x_k) m: 0 <= k <= n} is consistent, just using the hypotheses on
T, and no more. QED

COROLLARY. Let T be a consistent recursively axiomatizable extension of
EFA, possibly with additional sorts and p > 0. There is a constant c such
that for all n_1,...,n_p, "K(n_1) > c or ... or K(n_p) > c" is not provable
in T.

An interesting point is that EFA is probably insufficient to do Kolmogorov
complexity, as indicated below. However, K(n) > m makes perfectly good
sense in EFA.

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.

There is the question of just how to formalize iv). One can say that there
is a constant c such that for each n, there is a bit sequence x of length n
such that no program of length <= n+c yields x.

Here is a partial result.

THEOREM. EFA proves ii) implies Sigma-0-1 induction. PRA does not prove
i),ii),iii),iv). The same holds for any consistent extension of EFA by
Pi-0-2 sentences.

>> Under a standard presentation of K, roughly how big does c need to be for
>> ZFC? And what effect is there if we use PA (Peano Arithmetic) instead of
>> ZFC?
> :::
>> Again, under a standard presentation of Omega (i.e., a standard setup for
>> Turing machines), roughly how many digits can be determined in ZFC? And
>> what effect is there if we use PA (Peano Arithmetic) instead of ZFC?
>:::
>> But what if we fix the presentation of Turing machines to be reasonably
>> natural, in advance, and then change the theories?
>>
>> As a simplified example, suppose we are interested in the size of the
>> smallest Turing machine TM which does not halt but cannot be proved to not
>> halt in PA or ZFC. How do these sizes compare?
>
>RE: The problem here is that in general, we cannot compute these
>values (for a particular theory, with a particular coding of TMs and a
>particular Gödel numbering of its syntax, it may turn out to be
>possible to determine it )

I am raising the possibility of at least some comparison between PA and ZFC
on this basis.

>- actually Chaitin's methods only provide
>relatively loose upper bounds for them, contrary to what the
>standard interpretation seems to suggest. Indeed, if there were any
>kind of effective correspondence between F and the minimal c
>(etc.) for F, one could decide the Halting Problem.

If you use Turing machines, there are definite upper bounds as a function
of the number of symbols in F, assuming a standard version of predicate
calculus with equality. They aren't too bad, but noone wants to publish
good upper bounds because they aren't all that good, and the work is
tedious, and certaintly virtually infinitely difficult if one wants to cut
those bounds down somewhat. And for specific theories such as PA and ZFC,
such a project, if done really well, would probably make use of all kinds
of delicate constructions about which very few people know anything about.

>Compare: G2 provides an effective upper bound for the length of the
>shortest unprovable Pi-0-1 sentence in a give theory F, i.e.
>Length( Cons(F)) - but it gives absolutely no information about the
>simplest such unprovable sentence. And again, if there were a
>general method for finding the minimal unprovable Pi-0-1 sentence
>of a theory, one could decide the undecidable.

One could still be able to compute the exact value for PA using ZFC, or for
ZFC, using large cardinals. One could - not you or me.
>
>And as I have pointed out, there are acceptable codings in which
>these finite limits are the same for, say, PA and ZFC (or, for Q and
>ZFC+MC, or whatever) - and we simply do not know what happens
>with various "natural" or "standard" codings - as far as we know,
>they may still be the same, at least for some of them.  Or maybe
>not.

The level of robustness of various results in this area is really a major
issue - and an interesting one. I have some ideas for test questions - but
I won't go into this right now.
>
>Anyway, I guess - if it interests anybody - that for a standard
>coding technique, these values would turn out to be very large.

>But the
>reply to Harvey's question is: we do not know whether there is a
>difference, or whether it is the same TM.

I take this to mean a difference between PA and ZFC.