Re:proof nets for MLL with units

On Monday 26 April 2004 15:34, Alessio Guglielmi wrote:
> 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 believe that a proof is the formula tree plus "additional information". 
This is extremely vague, and it depends on the logic in question, what 
"additional information" means (it could even be the full sequent proof on 
top).

It is true that in our proof nets for MLL with units, and also for classical 
logic turns out to be some sort of linking of the leaves of the formula tree.
However, I consider this as a (lucky) coincidence. I take it by no means for 
granted that "simple decorations" do the job. I guess that as soon as we go 
to the first order (or second order) case, we will get much more 
sophisticated things.

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

I agree that a priori cut elimination has nothing to do with the identity of 
proofs. However, it turns out that for simple logics, like MLL or classical 
propositional, there is a simple notion of identity that is based on cut 
elimination, and that does the job. For MALL, MELL, full LL, of first order 
logic, the situation seems to be quite different.

-Lutz