[FOM] extramathematical notions and the CH
Timothy Y. Chow
tchow at alum.mit.edu
Fri Feb 1 14:13:07 EST 2013
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.
More information about the FOM