Proofs without syntax
Dominic Hughes · Annals of Mathematics · 2006
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 φ as a graph homomorphism h : C → G(φ), where G(φ) is a graph associated with φ and C is a coloured graph.The main theorem is soundness and completeness: φ is true if and only if there exists a combinatorial proof h : C → G(φ).Theorem 4.1 (Combinatorial Soundness and Completeness).A combinatorial proposition is true if and only if it has a combinatorial proof. Proof of Theorem 4.1The diagram below shows the dependency between the Lemmas (4.1-5.8) and Theorems (Ti.j) in this paper.T3.1 ' E T4.1 4.1 T5.2 ' 5.6 ' 5.3 E 5.4 E T5.