Subject: Re: Term syntax for derivations in Deep-Inference systems - msg#00007

Hello,

we are living exciting times: the war to bureaucracy has been declared, also from normally neutral countries like Switzerland.

Since Frogs grew quite a bit as of late, I thought that in order for everybody to follow the developments I should make available some material about this war and its weapons. You can read the two notes:

Formalism A: <http://iccl.tu-dresden.de/~guglielm/p/AG11.pdf>
Formalism B: <http://iccl.tu-dresden.de/~guglielm/p/AG13.pdf>

in addition to Stephane's and Kai's. The one on formalism B is simply the message I've sent to Frogs last February (at that time the list was not archived on Gmane).

The idea is to free proof theory from bureaucracy and come up with a bureaucracy-free *deductive* formalism, where bureaucracy means `inessential syntactic details' (notice that regular proof nets are not deductive). The word `bureaucracy' comes, of course, from Girard, but the methods we use are simpler and more effective than the ones Girard uses.

Some time ago I suggested a two-step movement: from CoS to formalism A and from formalism A to formalism B. The picture right now looks like a sort of continuum between CoS and semantics:

CoS <-> A <-> B =? ded. proof nets <-> proof nets <-> Tarski

Each <-> maintains properties between formalisms: for example, if A normalises, then B normalises, and if B normalises wrt properties that A possesses, then A normalises too wrt to those properties. I think that the game of identity of proofs will be played in the deductive proof nets arena, and I also think that deductive proof nets are the concrete representation of formalism B (probably obtained from relation webs, which are the ideal concrete representation of structures).

I have some quick preliminary comments on the two notes by Stephane and Kai, but for serious comments I need some more time to think.

First of all, I think Stephane's idea of using type judgments for describing the new formalisms is absolutely excellent, especially because it is super-clean.

That said, I also think that there is a difference between concrete derivations and their description by typing rules. One of our goals is to come up with geometric objects corresponding to proofs: these objects will be `concrete derivations', and they are intrinsically much more complex to be found than typing rules. However, since finding them means knowing their properties, typing rules are probably our best key to get where we want.

Comment for Stephane: I instinctively dislike the idea of associating inference rules to equations. I also have better reasons than just my instinct, for example the fact that invertibility of rules should be invisible to geometry (one could object about contraction and interaction but I have counter-objections; it's a long story).

Much better, I believe, integrating equations in typing rules, like in

A -M-> B B = C C -N-> D
--------------------------- .
A -M.N-> D

Is there any objection against this?

Comments for Kai: I still have to digest the very provocative title. I'll think about that.

You ask me whether I agree that your formalism is B. Ha! I gave no definition for B, and no name, how could I disagree? It looks like the main idea of B, i.e., inference rules operate on *derivations* is captured by your system.

There is one point, though, which makes me doubt a bit: you still need a distinction between formulae/structures and derivations, in the interaction rule. Pure B, whatever that is, should abolish the distinction, which means that we have to decide what is the negation of a derivation.

On the other hand, could be that your formalism succeeds in capturing and eliminating all bureaucracy without having to decide this difficult question. If this is so, it's very good, because we can postpone the decision until we know more.

Other comments as soon as I understand better, probably tomorrow night. Francois, what do you think?

-Alessio