Re: proof nets for MLL with units

Dear Alessio,

> > > 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.

> >I think so, and I'd go so far as to say that if a particular notion of
> >proof can be captured at all, it can be captured this way, but I think
> >this is a very risky way in which to proceed, because *any* information
> >at all might be added as `decoration'.  Indeed you never need to
> >decorate proofs, you can just decorate sequents, and make the rules
> >conditional on this decoration.  If you follow this route to its
> >ultimate end, you get labelled deduction.  There is then no way
> >internal to the framework to tell good from bad.

> I'm not following, I need a more explicit explanation. You seem to 
> talk about decorating proofs, while I was talking about decorating 
> formulas.

I had the idea that you shifted from talking about one to the other.
I think both are equally expressive.

> You take a formula, you decorate it and that captures all `identical' 
> proofs. This means: you check the decoration and you know you have a 
> proof of the formula; moreover, two `identical' proofs yield the same 
> decoration.

I had  misunderstood this.

> This is my (probably wrong) take of the mysticism surrounding proof 
> nets. Do you believe in this?

Not sure yet.  I'm persuadable that it can be done, I'm resistant to
the idea that this is the best way of thinking about the problem.  I
should add that I found Lutz's presentations appealing.

Charles