Re: How to use `deep inference'?

At 11:06 AM +0200 4/27/04, Lutz Strassburger wrote:
>On Monday 26 April 2004 18:16, Alessio Guglielmi wrote:
>>I agree only to a very, very limited extent, let's say I disagree:
>>for example, in the full system of linear logic, including 
>>exponentials, there is only one rule that escapes unified 
>>understanding, z_, all the others fit the one-rule-for-all scheme.
>
>But this is exactly the rule that deals with the exponentials. The 
>others that have exponentials in it are in fact rules for the 
>additives (they take care of the additive contraction).

Ha!, like in Cronenberg's `ExistenZ': this exponential only exists on 
the most pathetic level of reality.

I mean, you're right from your point of view, but your point of view 
is morally wrong!

You're considering linear logic as its *presentation* in the sequent 
calculus, and so you say: `in order to cope with *the way sequent 
calculus operates on additive contexts* (aka sort of a contraction) 
then I use exponentials, but I am just doing the additive 
context/contraction'.

My point of view is that linear logic exists independently of its 
badly flawed sequent calculus presentation, and that your 
presentation of it independently does the trick of deducing for it by 
using its connectives and modalities. I don't even want to know any 
more what is `additive', `multiplicative', etc., and if I see an 
exponential in an inference rule, well, for me that's just an 
exponential.

In other words, suppose you show me your system and a semantics for 
linear logic, and nothing else. You can easily convince me that you 
do have linear logic, but how much work will you need for convincing 
me that, for example, the rule

   `[?R,?T]'
   ---------
    ?`[R,T]'

is about a contraction?? (Without installing a bioport in my spine, I mean.)

>>In predicate logic, only instantiation, n_, falls outside of the 
>>scheme, but then, this is the minimum that has to be expected.
>
>Well, it is the only rule that actually does something to the 
>quantifiers. The others are either core rules or take care of 
>contraction. This is what I meant. We have a unified scheme for the 
>core and for the "taking-care-of-contraction-and-weakening"-non-core.

Same as above (with the difference that the sequent calculus 
presentation of classical logic is not badly flawed). Is

   [Ex.R,Ex.T]
   -----------
    Ex.[R,T]

about a contraction??

>Of course we have this regularity in the shape of the rules, 
>unifying all these different logics. But we still do not know where 
>this "method in the madness" comes from. I believe that there is a 
>deep reason for this, which is waiting for its discovery.

I might agree. Certainly, the subatomic thing will not tell us the 
reason. The only thing it will tell us, if I ever manage to make it 
work, is that in order to observe this total regularity one has to 
resort to a mysterious non-commutative world. It looks more like a 
puzzle than an explanation to me, but I would still be very happy if 
it worked just at the `phenomenological' level.

-Alessio