Konstantine Arkoudas
Abstract
The original proof of the four-color theorem by Appel and Haken sparked a controversy when Tymoczko used it to argue that the justification provided by unsurveyable proofs carried out by computers cannot be a priori. It also created a lingering impression to the effect that such proofs depend heavily for their soundness on large amounts of computation-intensive custom-built software. Contra Tymoczko, we argue that the justification provided by certain computerized mathematical proofs is not fundamentally different from that provided by surveyable proofs, and can be sensibly regarded as a priori. We also show that the aforementioned impression is mistaken because it fails to distinguish between proof search (the context of discovery) and proof checking (the context of justification). By using mechanized proof assistants capable of producing certificates that can be independently checked, it is possible to carry out complex proofs without the need to trust arbitrary custom-written code. We only need to trust one fixed, small, and simple piece of software: the proof checker. This is not only possible in principle, but is in fact becoming a viable methodology for performing complicated mathematical reasoning. This is evinced by a new proof of the four-color theorem that appeared in 2005, and which was developed and checked in its entirety by a mechanical proof system.
- Appel, K., & Haken, W. (1977). Every planar map is 4-colorable. Illinois Journal of Mathamatics, 21, 429-567.Google Scholar
Cross Ref
- Arkoudas, K. (2000). Denotational proof languages, PhD thesis, MIT, Department of Computer Science, Cambridge, USA. Google ScholarDigital Library
- Arkoudas, K. (2005). Simplifying proofs in Fitch-style natural deduction systems. Journal of Automated Reasoning, 34(3), 239-294. Google ScholarDigital Library
- Arkoudas K: n. d., Athena. http://www.pac.csail.mit.edu/athenaGoogle Scholar
- Bonjour, L. (1998). In defense of pure reason, Cambridge University Press.Google Scholar
- Burge, T. (1993). Content preservation. Philosophical Review, 102, 457-488.Google ScholarCross Ref
- Burge, T. (1998). Computer proof, apriori knowledge, and other minds. Noûs, 32, 1-37.Google ScholarCross Ref
- Chalmers, D. J. (1996). The conscious mind. Oxford University Press.Google Scholar
- Chisholm, R. (1989). Theory of knowledge (3rd Ed.). Prentice-Hall.Google Scholar
- Cohen, D. I. A. (1991). The superfluous paradigm. In J. H. Johnson & M. J. Loomes (Eds.), The mathematical revolution inspired by computing (pp. 323-329). Oxford: Clarendon Press.Google Scholar
- Coquand, T., & Huet, G. (1988). The calculus of constructions. Information and Computation, 76, 95- 120. Google ScholarDigital Library
- Detlefsen, M., & Luker, M. (1980). The four-color theorem and mathematical proof. The Journal of Philosophy, 77(12), 803-820.Google ScholarCross Ref
- Gonthier, G. (2005). A computer-checked proof of the four colour theorem http://www.research.microsoft.com/~gonthier/4colproof.pdfGoogle Scholar
- Kitcher, P. (1983). The Nature of mathematical knowledge. Oxford University Press.Google Scholar
- Kitcher, P. (2000). A priori knowledge revisited. In P. Boghossian & C. Peacocke (Eds.), New essays on the a priori. Oxford: Clarendon Press.Google Scholar
- MacKenzie, D. (1999). Slaying the kraken: The sociohistory of a mathematical proof. Social Studies of Science, 29(1), 7-60.Google ScholarCross Ref
- Rapaport, W. J. (1999). Implementation is semantic interpretation. The Monist, 82, 109-130.Google ScholarCross Ref
- Reichenbach, H. (1938). Experience and prediction. University of Chicago Press.Google Scholar
- Reynolds, J. C. (1998). Theories of programming languages. Cambridge University Press. Google ScholarDigital Library
- Rota, G.-C. (1997). The phenomenology of mathematical proof. Synthese, 111, 183-196.Google ScholarCross Ref
- Slaney, J. (1994). The crisis in finite mathematics: Automated reasoning as cause and cure. In A. Bundy (Eds.), Automated Deduction-CADE-12 (pp. 1-13). Springer: Berlin, Heidelberg. Google ScholarDigital Library
- Teller, P. (1980). Computer proof. The Journal of Philosophy, 77(12), 797-803.Google ScholarCross Ref
- Tymoczko, T. (1979). The four color theorem and its philosophical significance. The Journal of Philosophy, 76(2), 57-83.Google ScholarCross Ref
- Voronkov, A. (1995). The anatomy of Vampire: Implementing bottom-up procedures with code trees. Journal of Automated Reasoning 15(2).Google ScholarCross Ref
- Weidenbach, C. (2001). Combining superposition, sorts, and splitting, In: A. Robinson & A. Voronkov (Eds.), Handbook of automated reasoning, (Vol. 2). North-Holland. Google ScholarDigital Library
- Weizenbaum, J. (1976). Computer power and human reason, Freeman and Company. Google ScholarDigital Library
- Williams, B. A. O. (1972). Knowledge and reasons. In G. H. V. Wright (Ed.), Problems in the theory of knowledge (pp. 1-11). Springer.Google Scholar
Index Terms
- Computers, Justification, and Mathematical Knowledge
Recommendations
Paraconsistent Logic, Evidence, and Justification
In a forthcoming paper, Walter Carnielli and Abilio Rodrigues propose a Basic Logic of Evidence (BLE) whose natural deduction rules are thought of as preserving evidence instead of truth. BLE turns out to be equivalent to Nelson's paraconsistent logic ...
Introducing Justification into Epistemic Logic
Plato's tripartite definition of knowledge as justified true belief (JTB) is generally regarded as a set of necessary conditions for the possession of knowledge. The true belief components the JTB definition are represented in formal epistemology by ...
Justification Logic with Confidence
AbstractJustification logics are a family of modal logics whose non-normal modalities are parametrised by a type-theoretic calculus of terms. The first justification logic was developed by Sergei Artemov to provide an explicit modal logic for arithmetical ...
Comments