Proofs Without Syntax
摘要
"[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).
引用
@article{arxiv.math/0408282,
title = {Proofs Without Syntax},
author = {Dominic Hughes},
journal= {arXiv preprint arXiv:math/0408282},
year = {2007}
}
备注
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