[FOM] Proofs Without Syntax
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).
More information about the FOM