[FOM] Proofs Without Syntax

[Dominic Hughes]

``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
syntactic.

  http://boole.stanford.edu/~dominic/papers/proofs-without-syntax

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