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.

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 ----------------------------------------------------------------------------