Dear Russell:

You wrote:

>Why bound the proof?

It was not my idea.  Chaitin equated complexity with a computing program's 
length and a proof chain is a computing program according to Turing.

[rearranging your post]

>1+1=2, 2+1=3, 3+1=4 ...
>
>are all distinct theorems.

My view:

Again as in my response to Juergen these are not theorems but proof chains 
leading to theorems.

"3 + 1 =" is a proof chain using a theorem as its base.  It leads to the 
theorem "4 is a number"

"1 + 1 =" is the cascade founding proof chain and its base is the axiom "1 
is a number". It leads to the theorem "2 is a number".

>There can only ever be a finite number of independent theorems, in
>fact the number is equal to the number of axioms.

Since as I understand it overall proof chains start with an axiom then I agree.


>However, one can
>easily construct an infinite chain of theorems through logical
>operations:
>
>If T1, T2, T3 etc are theorems, then
>
>T4=T1 and T2, T5=T1 or T2, T6=T1 and T2 or T3, are also theorems.
>
>We can construct an infinite variety of these theorems.

You are writing programs and they have a complexity.  Chaitin limits this 
complexity to no more than the complexity of the FAS plus a constant.  Thus 
there can not be an infinite number of such constructions.

Hal


>Of course
>there will be many tautological relationships between the theorems,
>but they're still distinct theorems.

And finite in number.

Hal

Reply via email to