Philosophia Mathematica Advance Access published online on June 2, 2008
Philosophia Mathematica, doi:10.1093/philmat/nkn015
On Formally Measuring and Eliminating Extraneous Notions in Proofs
* Department of Philosophy, 201 Dickens Hall, Kansas State University, Manhattan, Kansas 66506–0803 U.S.A. aarana{at}ksu.edu
Many mathematicians and philosophers of mathematics believe some proofs contain elements extraneous to what is being proved. In this paper I discuss extraneousness generally, and then consider a specific proposal for measuring extraneousness syntactically. This specific proposal uses Gentzen's cut-elimination theorem. I argue that the proposal fails, and that we should be skeptical about the usefulness of syntactic extraneousness measures.
Thanks to Jeremy Avigad, David Corfield, Bruce Glymour, Marco Panza, Doug Patterson, and Neil Tennant for helpful comments on earlier versions of this paper.