Proofs Without Syntax

dc.creatorHughes, Dominic
dc.date2004-08-20
dc.date2006-07-18
dc.date.accessioned2026-07-07T06:38:44Z
dc.date.available2026-07-07T06:38:44Z
dc.description"[M]athematicians care no more for logic than logicians for mathematics." Augustus de Morgan, 1868. Proofs are traditionally syntactic, inductively generated objects. This paper presents an abstract mathematical formulation of propositional calculus (propositional logic) in which proofs are combinatorial (graph-theoretic), rather than syntactic. It defines a *combinatorial proof* of a proposition P as a graph homomorphism h : C -> G(P), where G(P) is a graph associated with P and C is a coloured graph. The main theorem is soundness and completeness: P is true iff there exists a combinatorial proof h : C -> G(P).
dc.descriptionAppears in Annals of Mathematics, 2006. 5 pages + references. Version 1 is submitted version; v3 is final published version (in two-column format rather than Annals style). Changes for v2: dualised definition of combinatorial truth, thereby shortening some subsequent proofs; added references; corrected typos; minor reworking of some sentences/paragraphs; added comments on polynomial-time correctness (referee request). Changes for v3: corrected two typos, reworded one sentence, repeated a citation in Notes section
dc.identifierhttps://arxiv.org/abs/math/0408282
dc.identifierhttp://arxiv.org/abs/math/0408282
dc.identifierAnnals of Mathematics, 2006
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/100843
dc.subjectLogic
dc.subjectCombinatorics
dc.subject03B05; 05C99
dc.titleProofs Without Syntax
dc.typetext

Files

Collections