Proofs without syntax. (English) Zbl 1130.03009

Hughes, Dominic J. D.

Ann. Math. (2) 164, No. 3, 1065-1076 (2006).

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

MSC:

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

Keywords:

propositional logic; combinatorial proof; graph homomorphism; soundness; completeness