[FOM] extramathematical notions and the CH

[Timothy Y. Chow]

On Fri, 1 Feb 2013, joeshipman at aol.com wrote:
> You didn't address MY crucial point: why do you "believe" the results of 
> a computer proof, for example the proof by Appel and Haken of the 
> 4-color map theorem or Hales's proof of the Kepler conjecture, if the 
> proof is too long to be humanly verified?

I did in fact address this point, albeit tersely, with my comment about 
finite versus infinite.

Pre-theoretically, we have a concept of finite verification.  By 
"pre-theoretic," I mean that the concept requires only very weak 
philosophical premises about naive realism.

Physical theories make predictions about the results of finite 
experiments, and we acquire confidence in them by performing the finite 
experiments.  All we really "know" are the results of finite experiments. 
The theories themselves are always tentative.

Now what about excessively long proofs?  In principle, all such proofs are 
finite, and are therefore of the *type* of thing that can be "known."  In 
practice, acquisition of this knowledge may require executing a procedure 
on a machine that may be built on advanced theoretical principles, as well 
as extrapolating those principles to a regime that may be slightly outside 
previously confirmed parameter ranges.  To the extent that belief of the 
computational result requires trusting that our physical theory can be so 
extrapolated, our "knowledge" is indeed somewhat uncertain.  And indeed, 
some people were uneasy about the Appel-Haken-Koch proof at first for 
more-or-less this reason, and there are some current skeptics about 
quantum computation that are also questioning the validity of 
extrapolating quantum theory beyond well-tested limits.  But as I said, at 
least we're not committing a category error by claiming that we "know," 
mathematically, the truth value of the four-color theorem, because the 
proof is a finite object.

On the other hand, your proposal goes beyond that, and suggests that we 
can *mathematically* "know" statements that are not even in principle the 
result of a finite verification in the pre-theoretical sense.  I maintain 
that this is a category error.

Let me try an analogy (this analogy isn't perfect so it might get me into 
trouble, but I'll try it anyway).  People sometimes make mistakes when 
writing proofs.  To the extent that an error might be present in the 
proof, we can't be "certain" that such-and-such a theorem is correct. 
Nevertheless, we are comfortable saying that we "know" that certain things 
are true, despite our background understanding of human fallibility.  Now 
suppose someone were to turn this around and say that the chances that 
something like the Riemann hypothesis or P != NP is false are smaller than 
the chances that there's a mistake in the proof of---I don't know---the 
latest hot theorem in the Annals of Mathematics, say, and therefore we're 
even more justified in saying that we "know" that the Riemann hypothesis 
is true.  I would cry foul.  That's changing the rules of the game. 
Whatever this new kind of knowledge is---Zeilberger might call it 
"semi-rigorous math"---it's not mathematical knowledge in the traditional 
sense, *even if* it's potentially more "certain" than some examples of 
traditional mathematical knowledge.

Tim