# [FOM] The unreasonable soundness of mathematics

Timothy Y. Chow tchow at alum.mit.edu
Sun May 15 16:26:34 EDT 2016

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