Proofs without syntax

DOI10.4007/ANNALS.2006.164.1065MaRDI QIDQ2469641zbMATH OpenOpenAlexFDO

Authors Dominic J. D. Hughes

Publication date 6 February 2008

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

Full work available at URL https://arxiv.org/abs/math/0408282, https://projecteuclid.org/euclid.annm/1172614620

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)

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).

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

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.
• scientific article; zbMATH DE number 2010094 (Why is no real title available?)
• 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
• Classical proof forestry
• scientific article; zbMATH DE number 7559288 (Why is no real title available?)
• scientific article; zbMATH DE number 7204450 (Why is no real title available?)
• 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
• Coherent interaction graphs
• Canonicity of proofs in constructive modal logic
• An Analytic Propositional Proof System on Graphs
• Proof nets for classical logic
• Combinatorial flows as bicolored atomic flows

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)