Proofs without syntax. (English) Zbl 1130.03009

Summary: 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\), 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\).


03B05 Classical propositional logic
03F07 Structure of proofs
05C15 Coloring of graphs and hypergraphs
05C70 Edge subsets with special properties (factorization, matching, partitioning, covering and packing, etc.)
05C75 Structural characterization of families of graphs
Full Text: DOI arXiv Euclid