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 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().