FOM: Re: Chaitin

[Raatikainen Panu A K]

On 25 Mar 01, at 15:27, JoeShipman at aol.com wrote:

> Rattikainen (with my comments in CAPS):
> 
> I strongly disagree. The easiest way is to use the notion of truth 
> and show by diagonal argument that provable does not exhaust 
> true. (see e.g. Smullyan's book on incompleteness). 
> 
> THIS IS NOT SO EASY, EXCEPT FOR SPECIALLY CHOSEN FORMAL SYSTEMS LIKE 
> SMULLYAN'S WHICH ARE DESIGNED FOR SELF-REFERENCE

RE: I am not sure if I understand this comment. I don't think that
PA etc. are in any way specially chosen or designed for self-reference. 

> Indeed, a 
> rigorous proof of Chaitin's theorem requires one to arithmetize both 
> Turing machines and the syntax of the theory in question (Gödel's 
> proof requires only the latter) and move back and forth between 
> these two codings (no wonder so many people have got lost).
> 
> WRONG.  FIRST OF ALL, ONCE YOU HAVE ARITHMETIZED TURING MACHINES YOU DON'T 
> NEED TO ARITHMETIZE SYNTAX, YOU CAN SIMPLY 
*PROGRAM* THE SYNTAX. 

RE: I am sorry to disagree: I submit that it makes no sense to talk 
about programming the syntax - in the context of Turing machines 
reading and writing only zeros and ones, which is the case in the 
algorithmic information theory - independently of a binary coding
of the syntax.

> SECONDLY, 
> YOU DON'T EVEN NEED TO ARITHMETIZE TURING MACHINES TO GET INCOMPLETENESS 
> RESULTS, JUST TO GET INCOMPLETENESS FOR PEANO ARITHMETIC WHICH IS MUCH 
> STRONGER.

RE: in a sense, yes (if I got your idea right - at least, if one has a 
theory that is about Turing machines directly). But in order to have 
interesting and generalized incompleteness results, there is no 
choice. 

(For those interested in details of what I mean by the claim that even
two codings are involved in Chaitin's theorem:see Section 3 of my JPL paper)

> CHAITIN'S APPROACH VIA THE HALTING PROBLEM MAKES IT VERY EASY TO SHOW THAT 
> ANY SOUND THEORY WHICH CAN FORMALIZE THE STATEMENTS K(m)>n IS INCOMPLETE.  

RE: to repeat myself a little: in order to formalize the statements 
K(m) > n" in an ordinary mathematical theory one has to 
arithmetize Turing machines first. After that, it is perhaps a 
subjective matter wheter one wants to call it "very easy" or not. 

But similarly, if one just assumes that a theory can formalize 
Prov(x) and Diagonalization and is sound, it is extremely easy to 
prove Gödel's first theorem fo such a theorem (see e.g. pages 827-
8 of Smorynski's Handbook survey; the proof takes just 6 lines).

> Further, the claim that "the strength of theories is ultimately
> dependent on their algorithmic information content is important" is 
> simply false, as Shipman's own comments later show when he 
> admits that "Some very strong theories seem to have much simpler 
> axiomatizations than much weaker ones" 
> 
> THAT IS WHY I USED THE WORDS 'ULTIMATELY' AND 'SEEM TO'.  IT IS WRONG TO 
> INTERPRET CHAITIN'S THEOREM TO MEAN THAT A STRONGER THEORY IS ALWAYS OF 
> GREATER ALGORITHMIC INFORMATION CONTENT THAN A WEAKER ONE.  THE POINT IS THAT 
> THE ALGORITHMIC INFORMATION CONTENT GIVES AN UPPER BOUND ON THE STRENGTH.

RE: I am glad we agree on the first point - and *this* is one of my 
key points  -  but this is what the standard interpretation of 
Chaitin's theorem has claimed. 

"Upper bound" - hmmm... perhaps something like this holds but I 
don't know how interesting it is anymore. Also, it may be  difficult 
to compare theories with different languages, say L(PA) and L(ZF).
Similarly, one could perhaps conclude that already length of a 
finitely axiomatizable theory gives an upper bound on the strength .

But my point has been that there is simply no correlation between 
complexity and strength, and I am afraid that such a talk about 
"upper bounds" may mislead one to believe that there is ...


* I hope I  managed to clarify my position above - but I am happy to 
continue the discussion .....

- Panu Raatikainen