[FOM] extramathematical notions and the CH

[Joe Shipman]

Tim,

I comprehend your distinction between "knowing" and "mathematically knowing", although I would not express it in those terms . You misunderstand me as follows:

I did not use the statement "mathematical knowledge" to mean "mathematically knowing" in the sense of having a humanly verified proof, even an "in-principle" verifiable proof which takes up so many megabytes or gigabytes of space that neither a single mathematician nor a collaboration of mathematicians can ever verify it in the traditional way. Rather, I used it in the sense "knowledge of mathematical statements", where the TYPE of knowing involved can be other than the traditional human verification of proofs. I am merely claiming that a mathematical statement which, if it were false, would have a very high AND CALCULABLE probability of contradicting an experimental result, can be said to be "known" in a useful sense, and furthermore, a sense that is not foreign to the experience of mathematicians.

Seven different examples of this last point, in the midst of which you are drawing a line which I claim is too arbitrary:

(1) Wiles's proof of the Fermat conjecture, which with a great deal of effort and some significant patching and interaction was verified by a sufficiently large group of sufficiently expert human mathematicians, as individuals

(2) The proof of the Classification of Finite Simple Groups, which is too large to be humanly verified by any individual mathematician, but which has after three decades of efforts by a large community of expert mathematicians achieved a stable consensus as proven.

(3) A "probabilistically checkable proof" as defined by computational complexity theorists, which can be regarded as an infeasibly large classical proof transformed into a humanly checkable combinatorial structure, such that if the proof is valid then humans randomly choosing portions of the structure to verify will succeed with high probability and if the proof is invalid then they will fail with high probability

(4a) A statement which can be probabilistically verified by a humanly performable calculation even if there is no short classical proof (primality testing used to be a good example of this until a real polynomial-time algorithm was discovered, but polynomial identity testing, which in complexity-theoretic terms is in BPP but not known to be in P, still works as an example).

(4b) A real proof like Appel and Haken's proof of the four-color map theorem, Hales's proof of the Kepler conjecture as enhanced by the "Flyspeck project" (not the original proof), or the enormous proof generated by Jonathan Schaeffer's "Chinook Project" that the game of checkers is a draw, which cannot be humanly verified in the traditional way but can be verified in the sense that the programs which generated the proof can be proved in the traditional way to be "correct programs" and other programs can be written which verify the output. Note that this differs from a "probabilistically checkable proof" in the non-uniformity of the verification; there might be a single error which invalidates the whole proof, which a feasible amount of human checking is very unlikely to detect, while PCPs are structured so that any such error is spread all over the proof and likely to be found by a feasible check.

(5) The verification by a quantum computer of a type clearly defined and understood, which depends on very well-established physics, that, with probability greater than (1 - 1/(10^100)), a certain mathematically defined function has a particular value. (There are no real examples of this yet but that is merely a technological issue; this differs from case 4a if BPP<BQP which is widely conjectured to be true, because in case 4a, where we have a BPP problem, there is a way a human can "simulate" the machine and achieve probabilistic confidence in a polynomial amount of time, or absolute confidence in an exponential amount of time).

(6) My speculation, except that the mathematical statement in question, while bearing the same epistemological relationship to experiment as case 5, is not an instance of a BQP problem which would be a Pi^0_0 statement, but rather a Pi^0_1 or Pi^0_2 statement which might have no ZFC proof. This is the form actual calculations of the predictions of experimental results in particle physics take, since they are generally represented numerically as a summation of infinitely many terms, and a measurement with a particular level of precision corresponds to the statement that the value of the infinite sum lies within a particular interval, a statement which, while mathematically well-defined, is of a logical type which makes it not necessarily decidable. The only reason this is different from case 5 is that in computational complexity theory,"quantum computers" have been defined in a particular and restricted way that can only solve problems that a Turing machine can solve, although possibly faster; but we may call a more general experimental setup a "quantum computer" also.

Note that I had to number these in a way that is only partially ordered--1, 2, 3, and 4b but not 4a satisfy your epistemological criterion of a finite proof object being generated, while 1, 2, 3, and 4a but not 4b satisfy the criterion that a human or group of humans, unaided by machines, can be satisfied with very high confidence in the truth of the statements. 

However, mathematicians recognize case 4a as a valid form of knowledge, because the error probability can be bounded, which distinguishes it from the Zeilbergerian scenario you cite which involves speculations about probabilities of mistakes; furthermore, your acceptance of case 4b because of the existence "in principle" of a proof object which can't possibly be surveyed in the traditional way, while justified because of the possibility of transforming such a proof into a PCP, also makes it more unreasonable to reject case 4a.

I claim that if you accept case 4a, the step to case 5 is sound, and it has already been taken by all the mathematicians who work in Quantum Complexity theory. Do you reject case 5? Or do you accept case 5 as describing valid "knowledge" of mathematical statements, but still reject case 6?

-- JS

Sent from my iPhone

On Feb 1, 2013, at 2:13 PM, "Timothy Y. Chow" <tchow at alum.mit.edu> wrote:


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