Show simple item record

dc.contributor.authorBundy, Alan
dc.contributor.authorJamnik, Mateja
dc.date.accessioned2018-09-20T12:07:38Z
dc.date.available2018-09-20T12:07:38Z
dc.date.issued2019
dc.identifier.issn2211-8136
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/280564
dc.description.abstractFollowing Hilbert, there seems to be a simple and clear definition of mathematical proof: it is a sequence of formulae each of which is either an axiom or follows from earlier formulae by a rule of inference. Automated theorem provers are based on this Hilbertian concept of proof, in which the formulae and rules of inference are represented in a formal logic. These logic- based proofs are typically an order of magnitude longer than the rigorous proofs produced by human mathematicians. There is a consensus, however, that rigorous proofs could, in principle, be unpacked into logical proofs, but this programme is rarely carried out because it would be tedious and uninformative. We argue that, for at least one class of rigorous proofs, which we will call schematic proofs, such a simple unpacking is not available. We will illustrate schematic proofs by analysing Cauchy’s faulty proof of Euler’s Theorem V-E+F = 2, as reported in [Lakatos, 1976] and giving further examples from [Nelsen, 1993]. We will then give a logic-based account of schematic proofs, distinguishing them from Hilbertian proofs, and showing why they are error prone.
dc.publisherSpringer International Publishing
dc.titleA Common Type of Rigorous Proof that Resists Hilbert’s Programme
dc.typeArticle
prism.endingPage71
prism.publicationDate2019
prism.publicationNameProof Technology in Mathematics Research and Teaching
prism.startingPage59
dc.identifier.doi10.17863/CAM.27932
dcterms.dateAccepted2018-07-03
rioxxterms.versionofrecord10.1007/978-3-030-28483-1_3
rioxxterms.licenseref.urihttp://www.rioxx.net/licenses/all-rights-reserved
rioxxterms.licenseref.startdate2019
dc.contributor.orcidJamnik, Mateja [0000-0003-2772-2532]
dc.identifier.eissn2211-8144
rioxxterms.typeJournal Article/Review
cam.issuedOnline2019-10-02
rioxxterms.freetoread.startdate2019-09-19


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record