The three dimensions of proofs

@misc{citeulike:2895473, 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.}, author = {Guiraud, Yves }, citeulike-article-id = {2895473}, eprint = {math/0612089}, keywords = {category-theory, logic, mathematics}, month = {Dec}, posted-at = {2008-06-15 07:25:44}, priority = {3}, title = {The three dimensions of proofs}, url = {http://arxiv.org/abs/math/0612089}, year = {2006} }

TY - ELEC ID - citeulike:2895473 L3 - citeulike-article-id:2895473 TI - The three dimensions of proofs N2 - 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. KW - category-theory KW - logic KW - mathematics AU - Guiraud, Yves PY - 2006/Dec/04/ UR - http://arxiv.org/abs/math/0612089 ER -