Proofs without syntax

Abstract

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\to 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\to G(\phi)$.