Sorry I missed this. Here is my response.
At , you wrote:
>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"
> >"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.
IMO it is a sequence of:
1) A formula which in this case is of the form ("data string" + ), it is a
rule of inference acting on a initializing theorem.
2) The initializing theorem is "data string". Let us ignore the fact that
the strings above are so short as to be individual alphabet elements.
3) The next step in the sequence is the axiom "1".
4) The value of this formula is designated by "=".
5) The value is the output string i.e. the theorem ("string" is a WFF)
which was just proven.
>If you interpret the theorem "4+1=5" as 5 is a number, how will you
>interpret 3+2=5 ?
It is another proof the theorem "string "5" is a number or WFF" [ Again
ignoring that this string is so short as to be a single alphabet
element.] There can be more than one proof of a theorem.
> >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
>Jacques Mallah answered this one. Actually it can be shown that there are
>arbitrary complex and lengthy proofs in all axiomatisation of
Yes, as I explained in a later post I was here making a mistake so I
explicitly added in the constraint I was using on a sub conscious level:
The comment is true of single valued programs or "deterministic" cascades.
> >"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
Well I think I fixed that as above.
>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.
That would be helpful.