Dear Russell: Yes we did indeed have a similar debate some time ago. At that time I was still trying to express this point of view correctly and admittedly made a number of mistakes back then [and still do]. Our debate helped me considerably and I thank you.
In response: I just posted a response to Juergen that may help. But here are a few comments. At 4/13/01, you wrote: >Basically, Hal believes a finite FAS by definition implies that each >theorem is constrained to be no more than N-bits in length. Well more precisely that the shortest possible proof chain of any theorem of a finite FAS can not be more complex than the limit which Chaitin provides. Is this not Chaitin's position? Given that, then there are only a finite number of theorems that satisfy this limit on the complexity of their shortest proof chains. >So by his >definition, number theory is not a finite FAS. That of course is one possible view if we allow theorem cascades. However, I prefer a more conservative view that this is an unresolved incompleteness that theorem cascades force towards completeness. >By contrast, almost everyone else believes finiteness in FASes refers >to a finite number of axioms, not that the theorems are bounded in any >fashion. Actually I believe that all the components of a finite FAS - axioms, rules, alphabet, and number of theorems must be finite. >Whilst I can appreciate diversity of viewpoints, I fail to see how >Hal's position actually yields a useful mathematical object. In >Juergen's chain below, what is the use of a system where a+1=b >(lets say) is a valid theorem, but b+1=c (where c=b+1=a+2) is an >invalid theorem because of an arbitrary cutoff rule? As I tried to show in my latest response to Juergen it seems to introduce a need for a random oracle which I believe you fell is an essential ingredient of SAS supporting universes. Hal
