[FOM] The unreasonable soundness of mathematics

[Timothy Y. Chow]

Daniel Mehkeri wrote:
> 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.)

Robinson's Q only appears to not have a problem to most of us because most 
of us are so used to understanding what "1, 2, 3, and so on" means that 
it's hard for us to notice when an implicit non-ultrafinitist assumption 
is being invoked.

The ultrafinitist or formalist or what have you has no trouble verifying 
the correctness of specific finite proofs in Q.  But what do the syntactic 
strings of Q *mean*?  Does the existence of proofs in Q imply anything 
about the integers or computation?  Not if the integers don't exist.

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

I do not want to get into debates about *what Nelson believed*, because 
then we can get entangled in debates about whether what Nelson believed 
was self-consistent, or sound, or whether the act of asserting that what 
Nelson believed might not have been sound is dishonoring to his memory. 
However, I'm happy to debate with *you*, if you wish to don an 
ultrafinitist hat.

The skill of being able to manipulate strings according to the rules of Q 
does not automatically imply a belief that said manipulations have 
anything meaningful to say about philosophical matters.  Do you (and when 
I say "you" I do not mean "Nelson" but rather "Mehkeri the ultrafinitist") 
believe that the existence of proofs of certain theorems of predicative 
arithmetic are philosophically relevant to the current debate?  How so? 
It is not enough to argue that Nelson thought that they were relevant; as 
I said, I don't want to argue about what Nelson thought.  I want to know 
what *you* think.

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

The theorem "sqrt(2) is irrational" is certainly proven.  The proof is 
finite and given explicitly and can be checked.  But I do not take it for 
granted that proven statements are *meaningful*, let alone *true*, even if 
they are proven in a weak system.  In particular, when you say that 
"sqrt(2) is irrational" means just what it says, I do not think that it is 
completely clear, to an ultrafinitist, what it says.  On the face of it, 
it appears to make an assertion about *infinitely many integers*---that 
among the infinitude of positive integers one cannot find A and B such 
that A^2=2*B^2.  But ultrafinitists do not generally believe in an 
infinitude of integers.  Do you, Mehkeri-qua-ultrafinitist, believe in an 
infinitude of integers?  If so, why do you still call yourself an 
ultrafinitist?  If not, then please spell out carefully what "sqrt(2) is 
irrational" means in terms that clearly do not implicitly assume an 
infinitude of integers.

My contention is that you can, for any feasible N, spell out in 
ultrafinitist terms what it means for there to not exist positive A and B 
less than N such that A^2=2*B^2, but that you cannot make the leap to 
asserting this for *all N* in the sense that non-ultrafinitists mean it. 
You have to take one feasible N at a time.  And it is therefore an 
unexplained mystery why, as you keep trying larger and larger values of N, 
the equation A^2=2*B^2 remains insoluble.

Tim