Re: How to use `deep inference'?

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

> In predicate logic, only instantiation, n_, falls outside of the
> scheme, but then, this is the minimum that has to be expected. In
> fact, (terms-in-)predicates have *nothing* to do with the
> propositional behaviour. On the contrary, I find it extremely
> remarkable that instantiation is the *only* rule that falls outside
> of the scheme!

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.

> It looks like you're downplaying what I consider our (and also your)
> biggest conceptual achievement, i.e., the fact that we took logics
> with a bunch of rules of totally different shapes and we shaped them
> into extremely regular objects.

Sorry if I made this impression. 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.

-Lutz