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

combinatorial proofcompletenessgraph homomorphismpropositional logicsoundness

Mathematics Subject Classification ID

Classical propositional logic (03B05) Structure of proofs (03F07) 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)

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

(29)

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

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)