Proofs without syntax

• Autores: Dominic J. D. Hughes
• Localización: Annals of mathematics, ISSN 0003-486X, Vol. 164, Nº 3, 2006, págs. 1065-1076
• Idioma: inglés
• DOI: 10.4007/annals.2006.164.1065
• Texto completo no disponible (Saber más ...)
• Resumen

  • 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 ¿Ó as a graph homomorphism h : C ¿¿ G(¿Ó), where G(¿Ó) is a graph associated with ¿Ó and C is a coloured graph. The main theorem is soundness and completeness: ¿Ó is true if and only if there exists a combinatorial proof h : C ¿¿ G(¿Ó).