Proofs Without Syntax

Preprint
Publisher Website
Google Scholar
  • 20 August 2004
Abstract
``Mathematicians care no more for logic than logicians for mathematics.'' [Augustus De Morgan, 1868] 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 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).

This publication has 0 references indexed in Scilit: