Proofs without syntax

• 成果类型: Article
• 署名作者: Hughes, Dominic J. D.
• 刊物名称: ANNALS OF MATHEMATICS
• ISSN/ISSBN: 0003-486X
• DOI: 10.4007/annals.2006.164.1065
• 发表日期: 2006
• 页码: 1065-1076
• 关键词: graphs

摘要

a 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 phi as a graph homomorphism h: C -> G(phi), where G(phi) is a graph associated with phi and C is a coloured graph. The main theorem is soundness and completeness: phi is true if and only if there exists a combinatorial proof h: C -> G(phi).