On Formally Measuring and Eliminating Extraneous Notions in Proofs

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.