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.

##
Advertising

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