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
Received on Fri Apr 13 2001 - 02:16:23 PDT
This archive was generated by hypermail 2.3.0
: Fri Feb 16 2018 - 13:20:07 PST