Re: proof nets for MLL with units

Hi,

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

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

Advisable, yes, never necessary.  Pervesity is exactly the risk.

Charles