Hostname: page-component-8448b6f56d-xtgtn Total loading time: 0 Render date: 2024-04-23T10:11:16.744Z Has data issue: false hasContentIssue false
  • English
  • Français

INFORMAL PROOF, FORMAL PROOF, FORMALISM

Published online by Cambridge University Press:  07 August 2015

ALAN WEIR
ALAN WEIR*
Affiliation:
Philosophy, University of Glasgow
*
*PHILOSOPHY, SGOIL NAN DAONNACHDAN OILTHIGH GHLASCHU\UNIVERSITY OF GLASGOW GLASGOW, G12 8QQ, SCOTLAND E-mail: Alan.Weir@glasgow.ac.uk
Get access Rights & Permissions [Opens in a new window]

Abstract

Increases in the use of automated theorem-provers have renewed focus on the relationship between the informal proofs normally found in mathematical research and fully formalised derivations. Whereas some claim that any correct proof will be underwritten by a fully formal proof, sceptics demur. In this paper I look at the relevance of these issues for formalism, construed as an anti-platonistic metaphysical doctrine. I argue that there are strong reasons to doubt that all proofs are fully formalisable, if formal proofs are required to be finitary, but that, on a proper view of the way in which formal proofs idealise actual practice, this restriction is unjustified and formalism is not threatened.

Type
Research Article
Information
The Review of Symbolic Logic , Volume 9 , Issue 1 , March 2016 , pp. 23 - 43
Copyright
Copyright © Association for Symbolic Logic 2015 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

BIBLIOGRAPHY

Awodey, S. (2010). Type theory and homotopy. Archived athttp://arxiv.org/abs/1010.1810.Google Scholar
Azzouni, J. (2004). The derivation-indicator view of mathematical practice. Philosophia Mathematica, 12, 81–105.Google Scholar
Azzouni, J. (2006). Tracking Reason: Proof, Consequence and Truth. Oxford: Oxford University Press.Google Scholar
Azzouni, J. (2009). Why do informal proofs conform to formal norms. Foundations of Science, 14, 9–26.Google Scholar
Baker, S., Ireland, A., & Smaill, A. (1992). On the use of the constructive omega rule within automated deduction. In Voronkov, A., editor. International Conference on Logic Programming and Automated Reasoning. Berlin: Springer, pp. 214–225.Google Scholar
Celluci, C. (2008). Why proof? what is proof? In Corsi, G. and Lupacchini, R., editors. Deduction, Computation, Experiment. Exploring the Effectiveness of Proof. Milan: Springer, pp. 1–27.Google Scholar
Cook, S., & Reckhow, R. (1979). The relative efficiency of propositional proof systems. The Journal of Symbolic Logic, 44, 36–50.Google Scholar
Field, H. (1989). Realism, Mathematics and Modality. Oxford: Blackwell.Google Scholar
Frege, G. (1903). Grundgesetze der Arithmetik II. Jena: Pohle. Reprinted in 1962, Hildesheim: George Olms. Translated in 2013 byEbert, P. A., & Rossberg, M. as Basic Laws of Arithmetic.Oxford: Oxford University Press.Google Scholar
Gabbay, M. (2010). A formalist philosophy of mathematics part I: Arithmetic. Studia Logica, 96, 219–238.Google Scholar
Goethe, N., & Friend, M. (2010). Confronting ideals of proof with the ways of proving of the research mathematician. Studia Logica, 96, 273–288.Google Scholar
Goodman, N., & Quine, W. V. O. (1947). Steps towards a constructive nominalism. Journal of Symbolic Logic, 12, 97–122.Google Scholar
Gowers, T. (2002). Mathematics: A Very Short Introduction. Oxford: Oxford University Press.Google Scholar
Horgan, T. (1994). Naturalism and intentionality. Philosophical Studies, 76, 301–26.Google Scholar
MacIntyre, A. (2005). The mathematical significance of proof theory. Philosophical Transactions of the Royal Society, 363, 2419–2435.Google Scholar
Marfori, M. A. (2010). Informal proofs and mathematical rigour. Studia Logica, 96, 261–272.CrossRefGoogle Scholar
Quine, W. V. O. (1995). From Stimulus to Science. Cambridge, Massachusetts: Harvard University Press.Google Scholar
Rav, Y. (1999). Why do we prove theorems? Philosophia Mathematica, 7, 5–41.Google Scholar
Rav, Y. (2007). A critique of a formalist-mechanist version of the justification of arguments in mathematicians’ proof practices. Philosophia Mathematica, 15, 291–320.Google Scholar
Tennant, N. (1997). The Taming of the True. Oxford: Clarendon Press.Google Scholar
Weir, A. (2010). Truth Through Proof – A Formalist Foundation for Mathematics. Oxford: Oxford University Press.Google Scholar
Wiedijk, F. (2008). Formal proof – getting started. Notices of the American Mathematical Society, 55, 1408–1414.Google Scholar