%0 Generic %1 Hughes2004 %A Hughes, Dominic %D 2004 %K proofs %T Proofs Without Syntax %U http://arxiv.org/abs/math/0408282 %X "Mathematicians 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).

@misc{Hughes2004, abstract = { "[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). }, added-at = {2011-01-24T10:52:57.000+0100}, author = {Hughes, Dominic}, biburl = {https://www.bibsonomy.org/bibtex/2aa50fe83d7ab244e9b2825b6d988032a/giuliano.losa}, description = {Proofs Without Syntax}, interhash = {69bad09a7ae2ed9158f2f97d1e9fbea2}, intrahash = {aa50fe83d7ab244e9b2825b6d988032a}, keywords = {proofs}, note = {cite arxiv:math/0408282 Comment: Appears 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}, timestamp = {2011-01-24T10:52:57.000+0100}, title = {Proofs Without Syntax}, url = {http://arxiv.org/abs/math/0408282}, year = 2004 }