Reliability of mathematical inference. (English) Zbl 1507.00016
Summary: Of all the demands that mathematics imposes on its practitioners, one of the most fundamental is that proofs ought to be correct. It has been common since the turn of the twentieth century to take correctness to be underwritten by the existence of formal derivations in a suitable axiomatic foundation, but then it is hard to see how this normative standard can be met, given the differences between informal proofs and formal derivations, and given the inherent fragility and complexity of the latter. This essay describes some of the ways that mathematical practice makes it possible to reliably and robustly meet the formal standard, preserving the standard normative account while doing justice to epistemically important features of informal mathematical justification.
MSC:
| 00A30 | Philosophy of mathematics |
References:
| [1] | Atiyah, M., Responses to: A. Jaffe and F. Quinn, “Theoretical mathematics: Toward a cultural synthesis of mathematics and theoretical physics”, Bulletin of the AMS, 30, 2, 178-207 (1994) · Zbl 0803.01014 · doi:10.1090/S0273-0979-1994-00503-8 |
| [2] | Avigad, J., Number theory and elementary arithmetic, Philosophia Mathematica, 11, 257-284 (2003) · Zbl 1050.03005 · doi:10.1093/philmat/11.3.257 |
| [3] | Avigad, J., Mathematical method and proof, Synthese, 153, 1, 105-159 (2006) · Zbl 1116.03012 · doi:10.1007/s11229-005-4064-5 |
| [4] | Avigad, J.; Mancosu, P., Understanding proofs, The philosophy of mathematical practice, 317-353 (2008), Oxford: Oxford University Press, Oxford · Zbl 1163.03001 · doi:10.1093/acprof:oso/9780199296453.003.0013 |
| [5] | Avigad, J. (in press). Modularity in mathematics. Review of Symbolic Logic. · Zbl 1439.00026 |
| [6] | Avigad, J., The mechanization of mathematics, Notices of the American Mathematical Society, 65, 6, 681-690 (2018) · Zbl 1398.68478 · doi:10.1090/noti1688 |
| [7] | Avigad, J.; Dean, E.; Mumma, J., A formal system for Euclid’s Elements, Review of Symbolic Logic, 2, 700-768 (2009) · Zbl 1188.03008 · doi:10.1017/S1755020309990098 |
| [8] | Avigad, J.; Harrison, J., Formally verified mathematics, Communications of the ACM, 57, 4, 66-75 (2014) · doi:10.1145/2591012 |
| [9] | Avigad, J.; Morris, R., Character and object, Review of Symbolic Logic, 9, 480-510 (2016) · Zbl 1427.01005 · doi:10.1017/S1755020315000398 |
| [10] | Azzouni, J., The derivation-indicator view of mathematical practice, Philosophia Mathematica, 12, 2, 81-105 (2004) · Zbl 1136.00301 · doi:10.1093/philmat/12.2.81 |
| [11] | Azzouni, J., Tracking reason (2006), Oxford: Oxford University Press, Oxford · Zbl 1094.03002 · doi:10.1093/acprof:oso/9780195187137.001.0001 |
| [12] | Azzouni, J., Why do informal proofs conform to formal norms?, Foundations of Science, 14, 1-2, 9-26 (2009) · Zbl 1182.03009 · doi:10.1007/s10699-008-9144-9 |
| [13] | Azzouni, J., The relationship of derivations in artificial languages to ordinary rigorous mathematical proof, Philosophia Mathematica, 21, 2, 247-254 (2013) · Zbl 1293.03006 · doi:10.1093/philmat/nkt007 |
| [14] | Azzouni, J.; Sriraman, B., Does reason evolve? (Does the reasoning in mathematics evolve?), Humanizing mathematics and its philosophy: Essays celebrating the 90th birthday of Reuben Hersh, 253-289 (2017), Cham: Springer, Cham · Zbl 1379.00019 · doi:10.1007/978-3-319-61231-7_20 |
| [15] | Bachmair, L.; Ganzinger, H.; Robinson, JA; Voronkov, A., Resolution theorem proving, Handbook of automated reasoning (in 2 volumes), 19-99 (2001), Amsterdam: Elsevier, Amsterdam · Zbl 0993.03008 · doi:10.1016/B978-044450813-3/50004-7 |
| [16] | Bourbaki, N. (1966). Éléments de mathématique. Fasc. XVII. Livre I: Théorie des ensembles. Hermann, Paris · Zbl 0141.00602 |
| [17] | Bratman, ME, Intention, plans, and practical reason (1999), Cambridge: Cambridge University Press, Cambridge |
| [18] | Burgess, JP, Rigor and structure (2015), Oxford: Oxford University Press, Oxford · Zbl 1434.00028 · doi:10.1093/acprof:oso/9780198722229.001.0001 |
| [19] | Dawson, JW Jr, Why prove it again? (2015), Cham: Springer, Cham · Zbl 1328.00096 · doi:10.1007/978-3-319-17368-9 |
| [20] | De Toffoli, S., ‘Chasing’ the diagram—the use of visualizations in algebraic reasoning, The Review of Symbolic Logic, 10, 1, 158-186 (2017) · Zbl 1417.00070 · doi:10.1017/S1755020316000277 |
| [21] | De Toffoli, S.; Giardino, V., Forms and roles of diagrams in knot theory, Erkenntnis, 79, 4, 829-842 (2014) · Zbl 1304.57013 · doi:10.1007/s10670-013-9568-7 |
| [22] | De Toffoli, S., & Giardino, V. (2015). An inquiry into the practice of proving in low-dimensional topology. In G. Lolli, G. Venturi, M. Panza (Eds.), From logic to practice (pp. 315-336). Cham: Springer. · Zbl 1429.00008 |
| [23] | De Toffoli, S., & Giardino, V. (2016). Envisioning transformations—the practice of topology. In B. Larvor (Ed.), Mathematical cultures (pp. 25-50). Cham: Birkhäuser/Springer. · Zbl 07907733 |
| [24] | Dedekind, R. (1996). Theory of algebraic integers. Cambridge: Cambridge University Press. A translation of Sur la théorie des nombres Entiers Algébrique (1877), translated and introduced by John Stillwell. · JFM 09.0126.01 |
| [25] | Detlefsen, M.; Gold, B.; Simons, RA, Proof: Its nature and significance, Proof and other dilemmas: Mathematics and philosophy, 3-32 (2008), Washington, D.C.: Mathematical Association of America, Washington, D.C. · Zbl 1163.00006 |
| [26] | Feferman, S. (1978). The logic of mathematical discovery vs. the logical structure of mathematics. In Philosophy of science association, East Lansing. Reprinted in In the light of logic, Oxford University Press, 1998 (pp. 77-93). |
| [27] | Ferreiros, J., Mathematical knowledge and the interplay of practices (2016), Princeton: Princeton University Press, Princeton · Zbl 1337.00015 · doi:10.1515/9781400874002 |
| [28] | Galois, E. (1962). Écrits et mémoires mathématiques. Gauthier-Villars, Paris. Edited by Robert Bourgne and Jean-Pierre Azra. · Zbl 0192.01502 |
| [29] | Gelbaum, BR; Olmsted, JMH, Counterexamples in analysis (1964), San Francisco: Holden-Day, San Francisco · Zbl 0121.28902 |
| [30] | Giaquinto, M., Visual thinking in mathematics: An epistemological study (2007), Oxford: Oxford University Press, Oxford · Zbl 1175.00023 · doi:10.1093/acprof:oso/9780199285945.001.0001 |
| [31] | Gonthier, G.; Asperti, A.; Avigad, J.; Bertot, Y.; Cohen, C.; Garillot, F.; Roux, S.; Mahboubi, A.; O’Connor, R.; Ould Biha, S.; Pasca, I.; Rideau, L.; Solovyev, A.; Tassi, E.; Théry, L.; Blazy, S.; Paulin-Mohring, C.; Pichardie, D., A machine-checked proof of the odd order theorem, Interactive theorem proving, 163-179 (2013), Berlin: Springer, Berlin · Zbl 1317.68211 · doi:10.1007/978-3-642-39634-2_14 |
| [32] | Hähnle, R.; Robinson, JA; Voronkov, A., Tableaux and related methods, Handbook of automated reasoning, 100-178 (2001), Amsterdam: Elsevier, Amsterdam |
| [33] | Hales, T., The Jordan curve theorem, formally and informally, American Mathematical Monthly, 114, 10, 882-894 (2007) · Zbl 1137.03305 · doi:10.1080/00029890.2007.11920481 |
| [34] | Hales, T.; Adams, M.; Bauer, G.; Dang, TD; Harrison, J.; Hoang, LT; Kaliszyk, C.; Magron, V.; McLaughlin, S.; Nguyen, TT; Nguyen, QT; Nipkow, T.; Obua, S.; Pleso, J.; Rute, J.; Solovyev, A.; Ta, THA; Tran, NT; Trieu, TD; Urban, J.; Vu, K.; Zumkeller, R., A formal proof of the Kepler conjecture, Forum of Mathematics, Pi, 5, e2 (2017) · Zbl 1379.52018 · doi:10.1017/fmp.2017.1 |
| [35] | Hamami, Y. (in press). Mathematical rigor and proof. Review of symbolic logic. · Zbl 1315.00044 |
| [36] | Hamami, Y., & Morris, R. (in press). Plans and planning in mathematical proofs. Review of Symbolic Logic. · Zbl 1482.00006 |
| [37] | Hamami, Y., Mumma, J., & Amalric, M. (2019). Euclidean diagrammatic reasoning as counterexample reasoning. Manuscript. |
| [38] | Hamami, Y.; Mumma, J., Prolegomena to a cognitive investigation of Euclidean diagrammatic reasoning, Journal of Logic, Language and Information, 22, 4, 421-448 (2013) · Zbl 1305.03008 · doi:10.1007/s10849-013-9182-8 |
| [39] | Johnson-Laird, PN, Mental models and human reasoning, Proceedings of the National Academy of Sciences, 107, 43, 18243-18250 (2010) · doi:10.1073/pnas.1012933107 |
| [40] | Lakatos, I., Proofs and refutations: The logic of mathematical discovery (1976), Cambridge: Cambridge University Press, Cambridge · Zbl 0334.00022 · doi:10.1017/CBO9781139171472 |
| [41] | Larkin, JH; Simon, HA, Why a diagram is (sometimes) worth ten thousand words, Cognitive Science, 11, 1, 65-100 (1987) · doi:10.1111/j.1551-6708.1987.tb00863.x |
| [42] | Larvor, B., How to think about informal proofs, Synthese, 187, 2, 715-730 (2012) · Zbl 1275.00022 · doi:10.1007/s11229-011-0007-5 |
| [43] | Larvor, B., Why the naïve derivation recipe model cannot explain how mathematicians’ proofs secure mathematical knowledge, Philosophia Mathematica, 24, 3, 401-404 (2016) · Zbl 1357.00020 · doi:10.1093/philmat/nkw012 |
| [44] | Lemmermeyer, F., Reciprocity laws: From Euler to Eisenstein (2000), Berlin: Springer, Berlin · Zbl 0949.11002 · doi:10.1007/978-3-662-12893-0 |
| [45] | Mac Lane, S., Mathematics. Form and function. (1986), New York: Springer, New York · Zbl 0666.00019 · doi:10.1007/978-1-4612-4872-9 |
| [46] | Mancosu, P., The philosophy of mathematical practice (2008), Oxford: Oxford University Press, Oxford · Zbl 1163.03001 |
| [47] | Manders, K.; Mancosu, P., The Euclidean diagram, The philosophy of mathematical practice, 80-133 (2008), Oxford: Oxford University Press, Oxford · Zbl 1163.03001 · doi:10.1093/acprof:oso/9780199296453.003.0005 |
| [48] | Marfori, MA, Informal proofs and mathematical rigour, Studia Logica, 96, 2, 261-272 (2010) · Zbl 1208.03011 · doi:10.1007/s11225-010-9280-4 |
| [49] | Morris, R. (in press). Motivated proofs: What they are, why they matter, and how to write them. Review of Symbolic Logic · Zbl 1437.00025 |
| [50] | Morris, R. (2015). Appropriate steps: A theory of motivated proofs. Ph.D. thesis, Carnegie Mellon University |
| [51] | Mumma, J., Constructive geometrical reasoning and diagrams, Synthese, 186, 1, 103-119 (2012) · Zbl 1274.03017 · doi:10.1007/s11229-011-9981-x |
| [52] | Pelc, A., Why do we believe theorems?, Philosophia Mathematica, 17, 1, 84-94 (2009) · Zbl 1182.03023 · doi:10.1093/philmat/nkn030 |
| [53] | Rav, Y., Why do we prove theorems?, Philosophia Mathematica, 7, 1, 5-41 (1999) · Zbl 0941.03003 · doi:10.1093/philmat/7.1.5 |
| [54] | Rav, Y., A critique of a formalist-mechanist version of the justification of arguments in mathematicians’ proof practices, Philosophia Mathematica, 15, 3, 291-320 (2007) · Zbl 1197.00026 · doi:10.1093/philmat/nkm023 |
| [55] | Rips, LJ, The psychology of proof: Deductive reasoning in human thinking (1994), Cambridge: MIT Press, Cambridge · Zbl 0850.68295 · doi:10.7551/mitpress/5680.001.0001 |
| [56] | Robinson, JA; Hölldobler, S., Proof \(=\) guarantee \(+\) explanation, Intellectics and computational logic, 277-294 (2000), Alphen aan den Rijn: Kluwer, Alphen aan den Rijn · Zbl 1001.03051 · doi:10.1007/978-94-015-9383-0_17 |
| [57] | Robinson, JA; Voronkov, A., Handbook of automated reasoning (in 2 volumes) (2001), Amsterdam: Elsevier, Amsterdam · Zbl 0964.00020 |
| [58] | Schlimm, D., Two ways of analogy: Extending the study of analogies to mathematical domains, Philosophy of Science, 75, 2, 178-200 (2008) · doi:10.1086/590198 |
| [59] | Schlimm, D., On the creative role of axiomatics. The discovery of lattices by Schröder, Dedekind, Birkhoff, and others, Synthese, 183, 1, 47-68 (2011) · Zbl 1235.00015 · doi:10.1007/s11229-009-9667-9 |
| [60] | Schlimm, D., Axioms in mathematical practice, Philosophia Mathematica, 21, 1, 37-92 (2013) · Zbl 1297.00022 · doi:10.1093/philmat/nks036 |
| [61] | Steen, LA; Seebach, JA Jr, Counterexamples in topology (1970), New York: Holt, Rinehart and Winston, New York · Zbl 0211.54401 |
| [62] | Tanswell, F., A problem with the dependence of informal proofs on formal proofs, Philosophia Mathematica, 23, 3, 295-310 (2015) · Zbl 1357.00027 · doi:10.1093/philmat/nkv008 |
| [63] | Tanswell, F. (2016). Proof, rigour and informality: A virtue account of mathematical knowledge. Ph.D. thesis, St. Andrews |
| [64] | Tappenden, J.; Mancosu, P.; Jorgensen, KF; Pedersen, SA, Proof style and understanding in mathematics I: Visualization, unification, and axiom choice, Visualization, explanation and reasoning styles in mathematics, 147-214 (2005), Berlin: Springer, Berlin · Zbl 1159.00310 · doi:10.1007/1-4020-3335-4_8 |
| [65] | Tignol, JP, Galois’ theory of algebraic equations (2016), Hackensack: World Scientific Publishing, Co. Pte. Ltd., Hackensack · Zbl 1333.12001 · doi:10.1142/9719 |
| [66] | Waszek, D.; Chapman, P.; Stapleton, G.; Moktefi, A.; Perez-Kriz, S.; Bellucci, F., Rigor and the context-dependence of diagrams: The case of Euler diagrams, Diagrammatic representation and inference (Diagrams 2018), 382-389 (2018), Cham: Springer, Cham · Zbl 1514.00020 · doi:10.1007/978-3-319-91376-6_35 |
| [67] | Wimsatt, WC, Re-engineering philosophy for limited beings: Piecewise approximations to reality (2007), Cambridge: Harvard University Press, Cambridge · doi:10.2307/j.ctv1pncnrh |
| [68] | Wussing, H. (1984). The genesis of the abstract group concept: a contribution to the history of the origin of abstract group theory. MIT Press, Cambridge, MA. Translated from the German by Abe Shenitzer and Hardy Grant. · Zbl 0547.01001 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
