[FOM] The unreasonable soundness of mathematics

[Timothy Y. Chow]

On Sat, 14 May 2016, Mario Carneiro wrote:
> Finally, once "for all feasible n, phi(n)" statements are regarded as 
> having ultrafinitist meaning, the "endless surprise" puzzle is resolved: 
> we have a single statement, which quantifies over all the numbers you 
> can hope to care about; the ultrafinitist is made to be convinced of 
> such a statement by translating an analogous pure mathematical statement 
> talking about "all n", with a finite and feasible proof. Having seen the 
> proof, the ultrafinitist will not be surprised by the gigabyte 
> computer's failure to find a counterexample, nor the terabyte computer.

It looks to me that the distinction you drew earlier in the conversation, 
between yourself and "true ultrafinitists," comes into play here.  Namely, 
the *formalization of feasible reasoning* seems relevant.

It sounds to me that you, Mario Carneiro (and not Mario Carneiro speaking 
for an ultrafinitist), are comfortable taking a traditional formal proof, 
that has no explicit "feasibility predicate," and glossing it line by line 
using the rule that when you see "An: phi(n)" then you read it out loud as 
"for all feasible n, phi(n)," and if Formal Statement X follows formally 
from Formal Statement Y according to traditional syntactic rules, then you 
accept that the "out-loud-reading" of Formal Statement X (i.e., its 
translation into a meaningful statement that explicitly involves the 
adjective "feasible") correctly follows from the "out-loud-reading" of 
Formal Statement Y.  Is that right?

However, it seems to me that a true ultrafinitist isn't entitled to this. 
The true ultrafinitist has to check whether the "out-loud-reading" of 
Formal Statement X follows from the "out-loud-reading" of Formal Statement 
Y *via ultrafinitistically valid logical reasoning*.

If one now tries to claim that there is a mechanical way of verifying 
whether X follows from Y via ultrafinitistically valid logical reasoning, 
then isn't that tantamount to claiming that there exists a satisfactory 
way to formalize ultrafinitistic reasoning?  But this was something you 
didn't want to claim.  (And I don't want to claim it myself, either---on 
this point we agree.)

So I am still left wondering how you make the leap from a formal 
verification that one formal statement follows *syntactically* from 
another, to a claim that one ultrafinitistically meaningful statement 
follows *logically* from another ultrafinistically meaningful 
statement---*without* claiming that there is a satisfactory way to 
formalize correct ultrafinitistic reasoning.

Tim