[FOM] Proofs Without Syntax

Dominic Hughes dominic at theory.stanford.edu
Thu Sep 2 14:55:00 EDT 2004

``Mathematicians care no more for logic than logicians for mathematics.'' 
                                               [Augustus De Morgan, 1868]

Proofs are traditionally syntactic, inductively generated objects.  The
paper below presents an abstract mathematical formulation of propositional
logic in which proofs are combinatorial (graph-theoretic), rather than


It is only 6 pages, and should be an easy read.  No background in graph
theory is required.

I would greatly welcome feedback from the FOM perspective.

The paper defines a *combinatorial proof* of a proposition P as a graph
homomorphism h : G -> G(P), where G(P) is a graph associated with P, and G
is a coloured graph. The main theorem is soundness and completeness: P is
true iff there exists a combinatorial proof h : G -> G(P).

Dominic Hughes
Stanford University

More information about the FOM mailing list