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.
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
