The three dimensions of proofs

Even though I am not completely sure if LTU is the appropriate place to discuss this paper by Yves Guiraud, I see no danger in posting it anyway.

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.

It discusses higher dimensional rewriting for SKS a deductive system for classical propositional logic in the style of the Calculus of Structures.
In intuitive sense this article has had a great appeal on me and I did not want to withhold it from the rest of us.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Thanks. This is of interest

Thanks. This is of interest to me.

Where's the kitchen sink?

And it's amazing that they have managed to include an aspect of every major area of mathematical interest I've had over the last couple years into one paper.

This will save me a lot of time... ;-)

More information on the subject


I came today for the first time on this site and I just saw this forum discussion. It's nice to see people interested into a paper of mine! Just for curiosity: Niels, how have you discovered it?

If you have any comment or question, I would be glad to hear, answer, discuss about this. Maybe this forum is not the right place for this, so you can reach me by email (address on my homepage, link in my profile).

Admittedly this subject is a

Admittedly this subject is a bit out of the mainstream for LtU, but I think it is not off-topic, so feel free to continue the discussion here.