[FOM] The unreasonable soundness of mathematics

[Daniel Mehkeri]

> Not quite.  As an ultrafinitist, I'll grant you the ability to
> specify a concrete computer with a specific, feasible number of
> components and a specific, feasible amount of memory.  The sticking
> point arises when generalizing/idealizing to an unbounded amount of
> memory.

> The classical mathematician is, on the basis of a *single* formal
> proof, making a prediction about the behavior of an unbounded number
> of concrete machines.  The ultrafinitist, on the other hand, has to
> separately build a megabyte-sized machine, a gigabyte-sized machine,
> a terabyte-sized machine, etc.,

I'd say we're talking about some version of formalism here, and
ultrafinitism doesn't imply this. Of course there's going to be a lot
of overlap. But formally, Robinson's Q wouldn't have this problem
representing abstract computation. (You might even say that was the
original point of Q.)

It's a shame Edward Nelson is no longer with us to speak for himself.
Well, I'll borrow his hat. You may recall he posted to FOM attempting
to prove the inconsistency of Peano Arithmetic (of Elementary
Recursive Arithmetic, in fact). So if anyone on FOM actually was an
ultrafinitist, I'd say it was him! On the other hand, his "predicative
arithmetic" started from Q.

Nelson had also written about religion, and I once wrote to him
specifically asking about an eternal afterlife and ultrafinitism. The
gist of his reply was, yes, it is eternal in the sense that there will
always be a next day. (And he quoted "Amazing Grace", which contains a
Grand Hotel paradox.) What he doubted was just that any of those days
would ever be numbered with some of the exponential notations we've
come up with.

So, I expect abstract computation was not a problem formally or
informally for him. Or, to take your earlier example, I expect he
would take "sqrt(2) is irrational" to mean just what it says. I also
expect he would hold it to be proven, since the standard proof of that
fact seems ultrafinitary and not at all problematic. It does not seem
to require the totality of exponentiation or anything like that.

Conversely, even if you were formalist to the point of denying the
meaning of abstract computation, you might still believe ERA and even
PA will not be proven inconsistent before humans go extinct. Actually
the original puzzle in this thread seems to be aimed at this sort of
person.

Regards,
Daniel Mehkeri