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)

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

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)