[FOM] The unreasonable soundness of mathematics

[Timothy Y. Chow]

Mulling over the recent FOM discussion I had with Mario Carneiro, I came 
up with an insight that I am going to call the "unreasonable soundness of 
mathematics", for reasons that should become clear.  I will start by 
posing a puzzle for ultrafinitists, but I will go on to pose a more 
general puzzle.

Let us start by picking some Pi_1 statement, such as "PA is consistent" or 
Fermat's Last Theorem (FLT).  What does such an assertion mean to an 
ultrafinitist?  As I understand it, there are two entirely different ways 
that an ultrafinitist might interpret such a statement.

Under the first interpretation, "PA is consistent" means something along 
the lines of, "When we program a computer in a certain way and set it 
running, we have never observed it to output `0=1', and furthermore nobody 
in the future will ever observe a similarly programmed computer to output 
`0=1', no matter how big a computer they build and no matter how patiently 
they wait."  Let's use the term "Computer A" to refer generically to 
computers that perform this kind of search for a counterexample to a Pi_1 
statement.

Under the second interpretation, "PA is consistent" is judged to be an 
infinitary mathematical statement which therefore has no "direct" meaning; 
instead, we make the sociological observation that mathematicians accept 
infinitary statements when and only when they are in possession of a 
*proof*.  Therefore when someone asserts "PA is consistent," they really 
mean something along the lines of, "It is an accepted fact in the 
mathematical community that if you take your favorite proof assistant and 
give it the appropriate input, then it will verify that there is a correct 
proof of Con(PA) in one of the generally accepted axiomatic systems for 
the foundations of mathematics."  Let's use the term "Computer B" to refer 
generically to computers that are equipped with proof assistants and that 
are dedicated to verifying formal proofs.

Which interpretation is favored might depend on who you ask, and in what 
context.  It might also depend on the Pi_1 statement in question.  For "PA 
is consistent" I suspect that most ultrafinitists will gravitate towards 
the first interpretation.  For FLT, I suspect that more ultrafinitists 
will gravitate towards the second interpretation, because they will 
hesitate to attribute direct semantic content to assertions about the 
integers.  It does not matter for what I say below which interpretation 
you prefer for which statements; the only important thing to note is that 
for Pi_1 statements, two entirely different readings are possible.

Now for the puzzle.  Most working mathematicians believe that there is a 
very close relationship between the activity of Computer A and the 
activity of Computer B.  For example, in the case of FLT, they believe 
that the proof of FLT *explains* why Computer A is failing to find a 
solution to the Fermat equation.  When they study the proof of FLT, their 
internal mental state gradually changes until they reach a point when they 
say they "understand" the proof, and at that point they arrive at a 
conviction that Computer A is doomed never to find a solution.  Note that 
this conviction is of a type that can never be achieved solely through 
empirical observation of Computer A---empirical observation alone can lead 
only to a "conjecture" and not a "theorem."  Computer B plays the role of 
verifying that the alleged proof satisfies certain conditions---or as we 
more commonly say, that the proof is "correct"---and hence its behavior 
contributes vitally to the *explanation* of the behavior of Computer A.

I claim that for the ultrafinitist, this behavior of working 
mathematicians is very puzzling.  Over time, the ultrafinitist can observe 
that the mathematical community is very good at predicting the results of 
certain computations, and that if asked for the source of their success, 
they reply by pointing to proofs.  For the ultrafinitist, however, *proofs 
have no semantic content*.  They do not make any assertions "about" 
anything.  Taken at face value, they appear to make assertions about 
integers and equations and elliptic curves and modular forms, but for the 
ultrafinitist such things do not "exist."  In particular, terms in a 
formal language do not refer to integrated circuits and flash drives and 
flatscreen monitors and the rest of the physical components of a computer. 
I claim that it is therefore totally mysterious why the activity of 
Computer B should have *anything at all to do* with explaining the 
behavior of Computer A.  This mystery I refer to as "the unreasonable 
soundness of mathematics."

The working mathematician is accustomed to *abstracting* the behavior of 
the physical computer and *reasoning* about the abstract objects, but the 
process of abstraction, or at least the resulting abstract object, is 
precisely what the ultrafinitist is skeptical about.  Indeed, we may 
recall Voevodsky's famous (or infamous?) talk, in which he seemed to 
suggest that perfectly correct proofs of "PA is consistent" in standard 
foundational systems give us no reason to believe that PA is consistent. 
I interpret Voevodsky to be arguing that in the case of "PA is 
consistent," the behavior of Computer B tells us nothing about the 
behavior of Computer A.  The only thing I would add is that there appears 
to be nothing special about "PA is consistent" in this regard.  It seems 
to me that if we share Voevodsky's skepticism, then we should also be 
skeptical that (for example) the standard proof that sqrt(2) is irrational 
tells us anything at all about what to expect if we program Computer A to 
search for positive integers X and Y such that X^2 = 2*Y^2.  In other 
words, it seems to me that the skeptical argument runs much deeper than 
any skepticism about specific axioms.

---

That concludes the first part of my discussion.  I would now like to 
suggest that the above viewpoint suggests a possible avenue for convincing 
the ultrafinitist to regard certain abstract mathematics as being real.

It seems to me that much of the skepticism about the existence of abstract 
infinitary objects has its roots in physical intuition.  That is, it is 
tacitly assumed that the acquisition of knowledge about physical objects 
through sense perception is a well-understood phenomenon.  After all, I 
have never heard anyone go on and on about the "unreasonable effectiveness 
of vision in providing knowledge about the physical universe"; it is not 
regarded as puzzling, and in need of further explanation, how human beings 
can possibly acquire knowledge of physical objects---or at least, it is 
regarded as much *less* puzzling than how we could possibly acquire 
knowledge of an abstract object such as an elliptic curve.  But if physics 
is regarded as a gold standard of some kind, then we can argue that 
knowledge of abstract objects is in fact entirely analogous to knowledge 
of physical entities that are not directly perceptible.  An "electron" in 
quantum field theory is not something that is directly accessible to our 
senses.  Rather, it is an *abstract* theoretical entity that is posited in 
order to explain the results of experiments, and it cannot even be 
correctly conceptualized in commonsense terms such as "particle" or 
"wave."  Similarly, elliptic curves are theoretical objects that are 
posited to explain the results of computer searches, and so we should not 
balk at accepting their reality any more than we should balk at accepting 
the reality of electrons.

---

Finally, let me address a potential objection.  In the past, I have 
complained that discussions about the "unreasonable effectiveness of 
mathematics in physics" rarely take the trouble to articulate what 
*reasonable* effectiveness would look like.  If we cannot give a clear 
account of how much effectiveness we can "reasonably" expect, then how can 
we be sure that the amount of effectiveness that we actually observe is 
really "unreasonable"?  Perhaps this is just another manifestation of the 
all-too-human tendency to see amazing patterns in randomness.  Similarly, 
someone might object that if one considers the connection between 
Computers A and B to be puzzling, then what on earth is *not* puzzling? 
Surely the proof that sqrt(2) is irrational is more of a gold standard for 
explanation than quantum field theory is, given that the latter is still 
riddled with mathematical gaps.

In response to this objection, I would raise the stakes and draw attention 
to Harvey Friedman's Pi_1 propositions that imply the 1-consistency of 
some large cardinal axiom and that are themselves implied by a slightly 
larger cardinal axiom.  Specifically, I ask, do the formal proofs of these 
propositions allow us to predict the behavior of the relevant Computer A 
with unshakable confidence?  I think that many people would balk here. 
But if you balk at large cardinal axioms, then what is your account of the 
relationship between Computer B and Computer A?  Are the proofs of 
Computer B doing more than just "explaining" the physical behavior of 
Computer A in the sense that physical theories "explain" physical 
phenomena?  If so, then in what sense are they doing more, and how do we 
pick which axioms to accept?  There seems to be some kind of puzzle here 
even for those who lack sympathy for the ultrafinitist position (though 
perhaps this is nothing than the usual puzzle of which axioms for 
mathematics to accept).

Tim