Let me try and short circuit this debate, since I had precisely this
debate with Hal about 18 months ago, where I found myself in the same
position Juergen finds himself now.

##
Advertising

Basically, Hal believes a finite FAS by definition implies that each
theorem is constrained to be no more than N-bits in length. So by his
definition, number theory is not a finite FAS.
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.
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?
Cheers
[EMAIL PROTECTED] wrote:
>
> > From: Hal Ruhl Thu Apr 12 14:07:54 2001
> >
> > In case what I tried to say was not clear the idea is that there are no
> > more than 2^(N + c) shortest possible unique proofs in an N-bit FAS. How
> > can number theory if it is a finite FAS contain an infinite number of
> > unique theorems?
>
> Hal, here is an infinite chain of provable unique theorems:
> 1+1=2, 2+1=3, 3+1=4, 4+1=5, ...
>
> Juergen
>
----------------------------------------------------------------------------
Dr. Russell Standish Director
High Performance Computing Support Unit, Phone 9385 6967
UNSW SYDNEY 2052 Fax 9385 6965
Australia [EMAIL PROTECTED]
Room 2075, Red Centre http://parallel.hpc.unsw.edu.au/rks
----------------------------------------------------------------------------