A problem with the dependence of informal proofs on formal proofs

Fenner Stanley Tanswell

Research output: Contribution to journalArticlepeer-review

45 Citations (Scopus)

Abstract

Derivationists, those wishing to explain the correctness and rigour of informal proofs in terms of associated formal proofs, are generally held to be supported by the success of the project of translating informal proofs into computer-checkable formal counterparts. I argue, however, that this project is a false friend for the derivationists because there are too many different associated formal proofs for each informal proof, leading to a serious worry of overgeneration. I press this worry primarily against Azzouni's derivation-indicator account, but conclude that overgeneration is a major obstacle to a successful account of informal proofs in this direction.
Original languageEnglish
Pages (from-to)295-310
Number of pages16
JournalPhilosophia Mathematica
Volume23
Issue number3
Early online date23 Mar 2015
DOIs
Publication statusPublished - Oct 2015

Fingerprint

Dive into the research topics of 'A problem with the dependence of informal proofs on formal proofs'. Together they form a unique fingerprint.

Cite this