[Date Index] [Thread Index] [FOM Postings] [FOM Home]

*To*: fom@math.psu.edu*Subject*: FOM: computer proofs*From*: Don Fallis <fallis@u.arizona.edu>*Date*: Thu, 03 Dec 1998 11:46:01 -0700*Sender*: owner-fom@math.psu.edu

Hi, The "ideal" procedure for mathematical justification is something like this: The mathematician writes down a sequence of statements. She then checks the statements one at a time to make sure that each statement is an axiom or follows from previous statements in the sequence. At the end of this procedure, the mathematician is justified in believing that the theorem is true (and that there is a proof of the theorem) because she knows the justification for each step of that proof. Of course, as D. Hume pointed out about 250 years ago, this is not a perfectly reliable source of justification. Mathematicians sometimes make mistakes. As a result, the mere fact that computers (and computer programmers) sometimes make mistakes does not identify an epistemic distinction between using computer proofs and using the "ideal" procedure. Even so, there is clearly an epistemic distinction between using computer proofs and using the "ideal" procedure. With a computer proof, a mathematician may be justified in believing that a theorem is true (and that there is a proof of the theorem), but not because she knows the justification for each step of her proof. (This is so regardless of whether or not the mathematician has proved the correctness of the program or even the correctness of the compiler.) Of course, as M. Detlefsen pointed out in the Journal of Philosophy about 20 years ago, the use of computer proofs is not the only way in which actual mathematical practice has diverged from the "ideal" procedure. For one thing, mathematicians sometimes do not know the justification for each step of their proofs because they sometimes rely on the expert testimony of other mathematicians. I imagine that many of the mathematicians who go on to derive consequences of FLT will be in just this epistemic position. Now, the formal study of proof (and the study of the foundations of mathematics in general) has given us a pretty comprehensive understanding of the epistemology of the "ideal" procedure. However, since mathematicians do not always follow the "ideal" procedure, I would submit that we do not have anywhere near a comprehensive understanding of how mathematicians are justified in believing the theorems that they have proved. Mathematical justification is a very mixed bag. A comprehensive epistemological account would have to include accounts of how people are justified in believing scientific facts about the physical world (e.g., facts about how computers work) and of how people are justified in believing testimony (which, by the way, is not a completely worked out issue among epistemologists) as well as a lot of other stuff. By the way, given this situation, I think that it is difficult to say with conviction that probabilistic proofs (which, like computer proofs, can provide mathematicians with indirect evidence of the existence of a formal proof) are epistemically inferior to the other stuff in this mixed bag. take care, don Don Fallis School of Information Resources & Library Science University of Arizona

[Date Prev] [Date Next] [Thread Prev] [Thread Next]

[Date Index] [Thread Index] [FOM Postings] [FOM Home]