The three dimensions of proofs
<|reference_start|>The three dimensions of proofs: 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.<|reference_end|>
@article{guiraud2006the,
    title={The three dimensions of proofs},
    author={Yves Guiraud},
    journal={Annals of Pure and Applied Logic, Volume 141, Issues 1-2, August
  2006, Pages 266-295},
    year={2006},
    doi={10.1016/j.apal.2005.12.012},
    archivePrefix={arXiv},
    eprint={math/0612089},
    primaryClass={math.CT cs.LO math.LO}
}