The Problem of Bureaucracy and Identity of Proofs from the Perspective of Deep Inference
Alessio Guglielmi · 2005
Deep inference offers possibilities for getting rid of much bureaucracy in deductive systems, and, correspondingly, to come up with interesting notions of proof identity. We face now the problem of designing formalisms which are intrinsically bureaucracy-free. Since we have a design problem, it is important to elaborate definitions that will remain useful for many years to come. I propose a discussion of several proposals. The discussion will hopefully be also a good way of introducing deep inference to those who don’t know it. In my talk I will explain in detail and with examples all the notions quickly sketched below. It is apparently extremely simple stuff, but there are subtle issues that only experienced proof theorists might appreciate; I will try to address them. The proposed solutions are currently discussed on the mailing list Frogs. By the time of the workshop, in addition to my proposed definitions, I will have also the opinions of the participants to the discussions. Bureaucracy and Identity Bureaucracy and identity of proofs are intimately related. There is no formal notion of bureaucracy, but I guess the consensus is that, when two proofs are morally the same, but they differ in inessential details, then this is due to bureaucracy. If this is so, we should conclude that eliminating bureaucracy should lead us to eliminate the inessential details that blur the `sameness , i.e., identity, of proofs. We should agree that, for any given logic, there are several possible notions of identity of proofs, and people can invent more and more of them. Given a notion of identity and a formalism, either the formalism is able to express the identical proofs or it isn't: in the latter case, we have bureaucracy, and we have an enemy. Our goal is to attack some specific, important kinds of bureaucracy, in order to improve the ability of proof theory to deal with bureaucracy. It is hopeless to try and define bureaucracy once and for all. However, it is now possible to define formalisms which get rid of the most brutal and medieval forms of bureaucracy.