%0 Journal Article
%T The three dimensions of proofs
%A Yves Guiraud
%J Mathematics
%D 2006
%I arXiv
%R 10.1016/j.apal.2005.12.012
%X 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.
%U http://arxiv.org/abs/math/0612089v1