Proofs without syntax

DOI10.4007/ANNALS.2006.164.1065zbMATH Open1130.03009arXivmath/0408282OpenAlexW2106988030MaRDI QIDQ2469641FDOQ2469641

Authors: Dominic J. D. Hughes 

Publication date: 6 February 2008

Published in: Annals of Mathematics. Second Series (Search for Journal in Brave)

Abstract: "[M]athematicians 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 : C -> G(P), where G(P) is a graph associated with P and C is a coloured graph. The main theorem is soundness and completeness: P is true iff there exists a combinatorial proof h : C -> G(P).

Full work available at URL: https://arxiv.org/abs/math/0408282

Recommendations

• From syntactic proofs to combinatorial proofs
• Proofs with graphs
• A new mapping between combinatorial proofs and sequent calculus proofs read out from logical flow graphs
• scientific article; zbMATH DE number 7204450
• On combinatorial proofs for modal logic

zbMATH Keywords

graph homomorphismcompletenesssoundnesspropositional logiccombinatorial proof

Mathematics Subject Classification ID

Classical propositional logic (03B05) Coloring of graphs and hypergraphs (05C15) Edge subsets with special properties (factorization, matching, partitioning, covering and packing, etc.) (05C70) Structural characterization of families of graphs (05C75) Structure of proofs (03F07)

Cited In (26)

• Discussing Hilbert's 24th problem
• The role of structural reasoning in the genesis of graph theory
• Complementary proof nets for classical logic
• A new mapping between combinatorial proofs and sequent calculus proofs read out from logical flow graphs
• Streams and strings in formal proofs.
• Title not available (Why is that?)
• From syntactic proofs to combinatorial proofs
• Combinatorial proofs for constructive modal logic
• Towards a combinatorial proof theory
• Towards Hilbert's 24th Problem: Combinatorial Proof Invariants
• Title not available (Why is that?)
• Title not available (Why is that?)
• Classical proof forestry
• Truth diagrams for some non-classical and modal logics
• Making proofs without Modus Ponens: An introduction to the combinatorics and complexity of cut elimination
• Combinatorial proofs and decomposition theorems for first-order logic
• Exponentially handsome proof nets and their normalization
• The explosion calculus
• Representing formulas of propositional logic by cographs, permutations and tables
• A semantic framework for proof evidence
• The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem
• Canonicity of proofs in constructive modal logic
• Coherent interaction graphs
• An Analytic Propositional Proof System on Graphs
• Combinatorial flows as bicolored atomic flows
• Proof nets for classical logic

This page was built for publication: Proofs without syntax

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2469641)