The three dimensions of proofs

DOI10.1016/J.APAL.2005.12.012MaRDI QIDQ2498912zbMATH OpenOpenAlexFDO

Authors Yves Guiraud

Publication date 16 August 2006

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

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

zbMATH Keywords

proof theoryclassical propositional logicstructural bureaucracythree-dimensional prooftranslation into polygraph

Mathematics Subject Classification ID

Classical propositional logic (03B05) Structure of proofs (03F07) Graphs, diagram schemes, precategories (18A10)

Abstract: In this document, we study a 3-polygraphic translation for the proofs of SKS, a formal system for classical propositional logic. We prove that the free 3-category generated by this 3-polygraph describes the proofs of classical propositional logic modulo structural bureaucracy. We give a 3-dimensional generalization of Penrose diagrams and use it to provide several pictures of a proof. We sketch how local transformations of proofs yield a non contrived example of 4-dimensional rewriting.

Recommendations

• Termination orders for three-dimensional rewriting
• Categorical proof theory of classical propositional calculus
• Coherence for Frobenius pseudomonoids and the geometry of linear proofs
• scientific article; zbMATH DE number 3946122
• scientific article; zbMATH DE number 1231506

Cites work

• scientific article; zbMATH DE number 195199 (Why is no real title available?)
• scientific article; zbMATH DE number 1924513 (Why is no real title available?)
• A system of interaction and structure
• Deep inference and symmetry in classical proofs
• Higher-dimensional word problems with applications to equational logic
• Linear logic
• MELL in the calculus of structures
• Term Rewriting and All That
• Termination orders for three-dimensional rewriting
• Towards an algebraic theory of Boolean circuits.
• Two polygraphic presentations of Petri nets

Cited in

(5)

• A topological perspective on interacting algebraic theories
• A folk model structure on omega-cat
• Polygraphic resolutions and homology of monoids
• Answers in search of a question: `proofs' of the tri-dimensionality of space
• Intensional properties of polygraphs

This page was built for publication: The three dimensions of proofs

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