Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Notes
Hamami (in press) does a particularly good job of clarifying the distinction between an informal foundation for mathematical reasoning and a formal one.
In his book, Re-engineering Philosophy for Limited Beings (Wimsatt 2007), William Wimsatt raises a similar concern about the robustness of long chains of reasoning in the context of scientific practice. See Chapter Four, titled “Robustness, Reliability, and Overdetermination.”
Pelc (2009) raises a more fundamental concern, namely, that complex theorems of mathematics may not have formal counterparts that can ever be verified mechanically by any processing device, given physical constraints such as the number of particles in the universe. But contemporary work in formal verification and interactive theorem proving establishes that they do, rather conclusively.
For an example of a fruitful interplay along these lines, see Hamami et al. (2019).
For example, even Philip Johnson-Laird, a foremost proponent of mental models, seems to acknowledge the use of inferential chains in solving logic problems (Johnson-Laird 2010, p. 5).
References
Atiyah, M., et al. (1994). 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.
Avigad, J. (2003). Number theory and elementary arithmetic. Philosophia Mathematica, 11, 257–284.
Avigad, J. (2006). Mathematical method and proof. Synthese, 153(1), 105–159.
Avigad, J. (2008). Understanding proofs. In P. Mancosu (Ed.), The philosophy of mathematical practice (pp. 317–353). Oxford: Oxford University Press.
Avigad, J. (in press). Modularity in mathematics. Review of Symbolic Logic.
Avigad, J. (2018). The mechanization of mathematics. Notices of the American Mathematical Society, 65(6), 681–690.
Avigad, J., Dean, E., & Mumma, J. (2009). A formal system for Euclid’s Elements. Review of Symbolic Logic, 2, 700–768.
Avigad, J., & Harrison, J. (2014). Formally verified mathematics. Communications of the ACM, 57(4), 66–75.
Avigad, J., & Morris, R. (2016). Character and object. Review of Symbolic Logic, 9, 480–510.
Azzouni, J. (2004). The derivation-indicator view of mathematical practice. Philosophia Mathematica, 12(2), 81–105.
Azzouni, J. (2006). Tracking reason. Oxford: Oxford University Press.
Azzouni, J. (2009). Why do informal proofs conform to formal norms? Foundations of Science, 14(1–2), 9–26.
Azzouni, J. (2013). The relationship of derivations in artificial languages to ordinary rigorous mathematical proof. Philosophia Mathematica, 21(2), 247–254.
Azzouni, J. (2017). Does reason evolve? (Does the reasoning in mathematics evolve?). In B. Sriraman (Ed.), Humanizing mathematics and its philosophy: Essays celebrating the 90th birthday of Reuben Hersh (pp. 253–289). Cham: Springer.
Bachmair, L., & Ganzinger, H. (2001). Resolution theorem proving. In J. A. Robinson & A. Voronkov (Eds.), Handbook of automated reasoning (in 2 volumes) (pp. 19–99). Amsterdam: Elsevier.
Bourbaki, N. (1966). Éléments de mathématique. Fasc. XVII. Livre I: Théorie des ensembles. Hermann, Paris
Bratman, M. E. (1999). Intention, plans, and practical reason. Cambridge: Cambridge University Press.
Burgess, J. P. (2015). Rigor and structure. Oxford: Oxford University Press.
Dawson, J. W, Jr. (2015). Why prove it again?. Cham: Springer.
De Toffoli, S. (2017). ‘Chasing’ the diagram—the use of visualizations in algebraic reasoning. The Review of Symbolic Logic, 10(1), 158–186.
De Toffoli, S., & Giardino, V. (2014). Forms and roles of diagrams in knot theory. Erkenntnis, 79(4), 829–842.
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.
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.
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.
Detlefsen, M. (2008). Proof: Its nature and significance. In B. Gold & R. A. Simons (Eds.), Proof and other dilemmas: Mathematics and philosophy (pp. 3–32). Washington, D.C.: Mathematical Association of America.
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).
Ferreiros, J. (2016). Mathematical knowledge and the interplay of practices. Princeton: Princeton University Press.
Galois, E. (1962). Écrits et mémoires mathématiques. Gauthier-Villars, Paris. Edited by Robert Bourgne and Jean-Pierre Azra.
Gelbaum, B. R., & Olmsted, J. M. H. (1964). Counterexamples in analysis. San Francisco: Holden-Day.
Giaquinto, M. (2007). Visual thinking in mathematics: An epistemological study. Oxford: Oxford University Press.
Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., et al. (2013). A machine-checked proof of the odd order theorem. In S. Blazy, C. Paulin-Mohring, & D. Pichardie (Eds.), Interactive theorem proving (pp. 163–179). Berlin: Springer.
Hähnle, R. (2001). Tableaux and related methods. In J. A. Robinson & A. Voronkov (Eds.), Handbook of automated reasoning (pp. 100–178). Amsterdam: Elsevier.
Hales, T. (2007). The Jordan curve theorem, formally and informally. American Mathematical Monthly, 114(10), 882–894.
Hales, T., Adams, M., Bauer, G., Dang, T. D., Harrison, J., Hoang, L. T., et al. (2017). A formal proof of the Kepler conjecture. Forum of Mathematics, Pi, 5, e2.
Hamami, Y. (in press). Mathematical rigor and proof. Review of symbolic logic.
Hamami, Y., & Morris, R. (in press). Plans and planning in mathematical proofs. Review of Symbolic Logic.
Hamami, Y., Mumma, J., & Amalric, M. (2019). Euclidean diagrammatic reasoning as counterexample reasoning. Manuscript.
Hamami, Y., & Mumma, J. (2013). Prolegomena to a cognitive investigation of Euclidean diagrammatic reasoning. Journal of Logic, Language and Information, 22(4), 421–448.
Johnson-Laird, P. N. (2010). Mental models and human reasoning. Proceedings of the National Academy of Sciences, 107(43), 18243–18250.
Lakatos, I. (1976). Proofs and refutations: The logic of mathematical discovery. Cambridge: Cambridge University Press.
Larkin, J. H., & Simon, H. A. (1987). Why a diagram is (sometimes) worth ten thousand words. Cognitive Science, 11(1), 65–100.
Larvor, B. (2012). How to think about informal proofs. Synthese, 187(2), 715–730.
Larvor, B. (2016). Why the naïve derivation recipe model cannot explain how mathematicians’ proofs secure mathematical knowledge. Philosophia Mathematica, 24(3), 401–404.
Lemmermeyer, F. (2000). Reciprocity laws: From Euler to Eisenstein. Berlin: Springer.
Mac Lane, S. (1986). Mathematics. Form and function. New York: Springer.
Mancosu, P. (Ed.). (2008). The philosophy of mathematical practice. Oxford: Oxford University Press.
Manders, K. (2008). The Euclidean diagram. In P. Mancosu (Ed.), The philosophy of mathematical practice (pp. 80–133). Oxford: Oxford University Press.
Marfori, M. A. (2010). Informal proofs and mathematical rigour. Studia Logica, 96(2), 261–272.
Morris, R. (in press). Motivated proofs: What they are, why they matter, and how to write them. Review of Symbolic Logic
Morris, R. (2015). Appropriate steps: A theory of motivated proofs. Ph.D. thesis, Carnegie Mellon University
Mumma, J. (2012). Constructive geometrical reasoning and diagrams. Synthese, 186(1), 103–119.
Pelc, A. (2009). Why do we believe theorems? Philosophia Mathematica, 17(1), 84–94.
Rav, Y. (1999). Why do we prove theorems? Philosophia Mathematica, 7(1), 5–41.
Rav, Y. (2007). A critique of a formalist-mechanist version of the justification of arguments in mathematicians’ proof practices. Philosophia Mathematica, 15(3), 291–320.
Rips, L. J. (1994). The psychology of proof: Deductive reasoning in human thinking. Cambridge: MIT Press.
Robinson, J. A. (2000). Proof \(=\) guarantee \(+\) explanation. In S. Hölldobler (Ed.), Intellectics and computational logic (pp. 277–294). Alphen aan den Rijn: Kluwer.
Robinson, J. A., & Voronkov, A. (Eds.). (2001). Handbook of automated reasoning (in 2 volumes). Amsterdam: Elsevier.
Schlimm, D. (2008). Two ways of analogy: Extending the study of analogies to mathematical domains. Philosophy of Science, 75(2), 178–200.
Schlimm, D. (2011). On the creative role of axiomatics. The discovery of lattices by Schröder, Dedekind, Birkhoff, and others. Synthese, 183(1), 47–68.
Schlimm, D. (2013). Axioms in mathematical practice. Philosophia Mathematica, 21(1), 37–92.
Steen, L. A., & Seebach, J. A, Jr. (1970). Counterexamples in topology. New York: Holt, Rinehart and Winston.
Tanswell, F. (2015). A problem with the dependence of informal proofs on formal proofs. Philosophia Mathematica, 23(3), 295–310.
Tanswell, F. (2016). Proof, rigour and informality: A virtue account of mathematical knowledge. Ph.D. thesis, St. Andrews
Tappenden, J. (2005). Proof style and understanding in mathematics I: Visualization, unification, and axiom choice. In P. Mancosu, K. F. Jorgensen, & S. A. Pedersen (Eds.), Visualization, explanation and reasoning styles in mathematics (pp. 147–214). Berlin: Springer.
Tignol, J. P. (2016). Galois’ theory of algebraic equations (2nd ed.). Hackensack: World Scientific Publishing, Co. Pte. Ltd.
Waszek, D. (2018). Rigor and the context-dependence of diagrams: The case of Euler diagrams. In P. Chapman, G. Stapleton, A. Moktefi, S. Perez-Kriz, & F. Bellucci (Eds.), Diagrammatic representation and inference (Diagrams 2018) (pp. 382–389). Cham: Springer.
Wimsatt, W. C. (2007). Re-engineering philosophy for limited beings: Piecewise approximations to reality. Cambridge: Harvard University Press.
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.
Acknowledgements
I am grateful to Silvia De Toffoli, Yacin Hamami, and three anonymous reviewers for helpful comments and suggestions. This work has been partially supported by AFOSR Grant FA9550-18-1-0120 and the Sloan Foundation.
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
About this article
Cite this article
Avigad, J. Reliability of mathematical inference. Synthese 198, 7377–7399 (2021). https://doi.org/10.1007/s11229-019-02524-y
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11229-019-02524-y