[FOM] Monsieur, x^p = x (mod p), donc Dieu existe. Repondez !

[Vaughan Pratt]

On 3/10/2011 6:55 PM, Daniel Mehkeri wrote:
 > Now, it might be thought there could be an alternate ultrafinitary
 > proof. Here is a reason to think otherwise: suppose for example
 > Bounded Arithmetic could prove it.

For us nonparticipants in this game it would be helpful to know the 
ground rules.

I heard Yessenin-Volpin talk on his version of ultrafinitism at MIT in 
the 1970s.  While it did not make sense to me then, it occurs to me now 
that one might base such a notion on the Blum axioms (q.v. on Wikipedia) 
for a choice of complexity measure on an acceptable Goedel numbering of 
the partial recursive functions, along with a plausible limit on how 
long a program can run, such as some estimate of the lifetime to date of 
the universe in Planck time units, or (much) more generously Parikh's 
number 2^1000.  In particular one can imagine proving that there must be 
only finitely many feasible numbers in a suitable (but non-vague) sense, 
hence a least infeasible number and a greatest feasible number.  What 
has been accomplished along such lines?

Anything less general would seem to smack of arbitrariness, while 
anything more general would seem hard to prove however defined.

Vaughan Pratt