Dear Russell:
You wrote:

##
Advertising

>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