Hal Ruhl wrote:
>>Juergen: Hal, here is an infinite chain of provable unique theorems:
>> 1+1=2, 2+1=3, 3+1=4, 4+1=5, ...
>
>First these are not theorems they are proof chains ending in theorems.

##
Advertising

If you reinterpret Juergen's word then you can tell him anything.
In all presentations of arithmetics I have seen proposition like "4+1 = 5"
are theorems.
>"4 + 1 =" is a proof chain and the theorem proved is: "5" is a number.
In what sense "4+1=" is a proof chain ? A proof must be a sequence of
formula each of which are either axiom instance or theorems.
If you interpret the theorem "4+1=5" as 5 is a number, how will you
interpret 3+2=5 ?
>Since most strings of length L are not
>compressible and have a complexity on the order of L + H(L) eventually the
>cascade will encounter a base theorem string that makes the proof chain
>itself too complex to fit into a number theory of a given finite
>complexity.
Jacques Mallah answered this one. Actually it can be shown that there are
arbitrary complex and lengthy proofs in all axiomatisation of
elementary arithmetic.
>"If a FAS is consistent and finite and doing arithmetic it is incomplete"?
That is true. You can even weaken "finite" with "countable".
>So Godel is already a corollary of Turing and perhaps of Chaitin as well.
Godel first incompleteness theorem is indeed easy to derive from
Turing works on Non-Halting machines.
Although Chaitin presents its work as a generalisation of Godel, I
would say it is half true. Godel gives a constructive proof of the
existence of an undecidable statement in (all) axiomatisable formal
systems. Chaitin gives a non constructive proof of the existence
of an infinity of undecidable statements (linked with the notion
of complexity).
I think that those who reason with formal systems should take
standart one and gives the precise presentation of it, or point
toward it through, perhaps some bibliographical links.
Bruno