On Formally Measuring and Eliminating Extraneous Notions in Proofs

Philosophia Mathematica 17 (2):189-207 (2009)
  Copy   BIBTEX

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.

Categories

Keywords

Reprint years

DOI

10.1093/philmat/nkn015

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,783

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

A Reverse Analysis of the Sylvester-Gallai Theorem.Victor Pambuccian - 2009 - Notre Dame Journal of Formal Logic 50 (3):245-260.
Eliminating the ordinals from proofs. An analysis of transfinite recursion.Edoardo Rivello - 2014 - In Proceedings of the conference "Philosophy, Mathematics, Linguistics. Aspects of Interaction", St. Petersburg, April 21-25, 2014. pp. 174-184.
Deepening the Automated Search for Gödel's Proofs.Adam Conkey - unknown
Probabilistic proofs and transferability.Kenny Easwaran - 2009 - Philosophia Mathematica 17 (3):341-362.
Aspects of Mathematical Explanation: Symmetry, Unity, and Salience.Marc Lange - 2014 - Philosophical Review 123 (4):485-531.
A Formally Verified Proof of the Prime Number Theorem.Jeremy Avigad, Kevin Donnelly, David Gray & Paul Raff - 2007 - ACM Transactions on Computational Logic 9 (1).
Normalization and Cut-Elimination in First-Order Logic.Anthony Michael Ungar - 1986 - Dissertation, Stanford University
Piety and the Proofs.John Clayton - 1990 - Religious Studies 26 (1):19 - 42.
Why do mathematicians re-prove theorems?John W. Dawson Jr - 2006 - Philosophia Mathematica 14 (3):269-286.
The Depth of Resolution Proofs.Alasdair Urquhart - 2011 - Studia Logica 99 (1-3):349-364.
On the Proof-Theory of two Formalisations of Modal First-Order Logic.Yehuda Schwartz & George Tourlakis - 2010 - Studia Logica 96 (3):349-373.
A Problem with the Dependence of Informal Proofs on Formal Proofs.Fenner Tanswell - 2015 - Philosophia Mathematica 23 (3):295-310.
Duplication of directed graphs and exponential blow up of proofs.A. Carbone - 1999 - Annals of Pure and Applied Logic 100 (1-3):1-67.
On Bellert's proposal concerning quantificational universals.Zygmunt Vetulani - 1987 - Studia Logica 46 (4):311-320.
The Nature and Relation of the Three Proofs of God's Existence in Descates' Meditations.David N. Stamos - unknown

Analytics

Added to PP
2009-01-28

Downloads
130 (#140,357)

6 months
14 (#178,038)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Andrew Arana
Université de Lorraine

Citations of this work

On the relationship between plane and solid geometry.Andrew Arana & Paolo Mancosu - 2012 - Review of Symbolic Logic 5 (2):294-353.
The Calculus of Natural Calculation.René Gazzari - 2021 - Studia Logica 109 (6):1375-1411.
Ontological Purity for Formal Proofs.Robin Martinot - forthcoming - Review of Symbolic Logic:1-40.

View all 9 citations / Add more citations

References found in this work

The foundations of arithmetic.Gottlob Frege - 1884/1950 - Evanston, Ill.,: Northwestern University Press.
Basic proof theory.A. S. Troelstra - 1996 - New York: Cambridge University Press. Edited by Helmut Schwichtenberg.
Proof theory.Gaisi Takeuti - 1975 - New York, N.Y., U.S.A.: Sole distributors for the U.S.A. and Canada, Elsevier Science Pub. Co..
Proof Theory.Gaisi Takeuti - 1990 - Studia Logica 49 (1):160-161.

View all 16 references / Add more references