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
