On Formally Measuring and Eliminating Extraneous Notions in Proofs
Andrew Arana · Philosophia Mathematica · 2008
ABSTRACT. 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. Many mathematicians and philosophers of mathematics think that it’s somehow valuable for a proof to be “pure”, that is, for it not to use notions extraneous to what is being proved. Not worrying about why that is for now, we would like to make better sense of the suggestion. What does it mean for a notion used in a proof to be extraneous to the theorem being proved? One way of making this sharper would be to develop a syntactic way of evaluating extraneousness. I want to consider such a proposal, using Gerhard Gentzen’s cut-elimination theorem. I will argue that there are serious obstacles to making this proposal work. 1. FOUR CLAIMS CONCERNING EXTRANEOUSNESS Bertrand’s postulate states that for every natural number n ≥ 1, there is a prime number between n and 2n. It is so named because it was verified by computation for