Re:proof nets for MLL with units

At 13:07 +0200 26.4.04, Lutz Strassburger wrote:
>A proof net should capture the essence of a proof such that two "morally
>identical" proofs are represented by the same object. Of course, the question
>is what is "morally identical". People usually consider here "up to trivial
>rule permutations in the sequent calculus". In this paper we do in principle
>the same. But there is one conceptual difference to Girards perception of
>what a proof net is. In Girards sense a proof net is a graph-like
>presentation of a sequent proof, where each rule gets a link assigned to it.
>This works well for MLL, badly for MALL and MELL, and not at all for the
>units, not to speak of classical logic.
>
>In our perception a proof net is a graph like thing containing the formula
>tree plus some "additional information". What this "additional information"
>is, depends on the logic in question. For MLL without units, it is simply the
>axiom links. If we add the units, we get more sophisticated linkings. This is
>what the paper is about.

Nothing to do specifically with Lutz's and Francois's paper, which I 
like a lot:

I'd like to know whether people believe or not that identity of 
proofs in sophisticated logics, like classical logic, can effectively 
be captured by simple `decorations' on top of the formula tree.

My gut feeling is that some more `deductive' information will be 
necessary or convenient. In other words, encoding the entire 
deductive information of a, say, sequent calculus proof, in linkings 
and boxes might be possible, but could very easily be perverse, and 
so inconvenient, one way or another.

My (certainly naif!) point of view is that proof nets should *easily* 
correspond to normal deductive proofs, but in a formalism that 
doesn't force unnecessary permutations. As a further property, they 
should preserve `identity' through some form of normalisation, sure. 
And, by the way, this will definitely not be cut elimination!! This 
is another perversion dictated by our current (soon to be over) 
misery. (What I'm trying to do with my formalisms `A' and `B' is 
setting up a principled approach to this problem.)

-Alessio