Re: proof nets for MLL with units

Charles:

At 7:21 +0000 5.5.04, Charles Stewart 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 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.

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.

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


Lutz:

This time I agree with almost everything you're saying. For the sake 
of completeness:

At 18:24 +0200 5.5.04, Lutz Strassburger wrote:
>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).

The full sequent proof on top is not a good answer because it would 
entail a trivial notion of identity of proofs, which I required. 
Actually, asking for a nontrivial such notion removes a lot of the 
vagueness from this situation, I believe.

-Alessio