Re: How to use `deep inference'?

At 21:02 +0200 28.4.04, Lutz Strassburger wrote:
>I never said that I want to replace any rule by contraction an weakening. I
>just made the stupid little observation that those rules that follow the
>scheme can be replaced by weakening and contraction (and therefore they are
>sound), and asked the question whether there is a way of bringing some order
>into the others. Let me repeat that I am not making any moral point out of
>it.

Your little observation is not so innocent, because it implies that 
we are in a mess, while we brought order already and we are going to 
bring even more. I wonder why you make such a claim after having been 
one of those that more contributed to finding this WONDERFUL order.

You shouldn't be surprised if I react to your saying

>All we have so far is the "recipe for the core", and some vague idea 
>for the non-core, provided it is weakening and contraction. Alessio, 
>any news about subatomic logic?

by explaining that we have a bit more than just a vague idea and 
that, luckily, this has little to do with weakening and contraction. 
(Weakening and contraction *do not* bring order, quite the 
opposite!!) BTW, what about identity and cut? they also are non-core; 
do you agree on what I wrote in my subatomic note?

You could say that you don't want to deal with subatomic particles, 
fine, but then what about Charles, Phiniki and Robert? They are 
designing systems for modal logics and geometric theories, and I 
guess they don't see themselves as cutting their way through the 
jungle by using a machete. I know a bit the work of Pietro on 
noncommutative logic and he doesn't seem to produce monsters either. 
If I compare this with the sequent calculus I see much, much more 
order.

You say now that you don't want to make a moral point out of your 
observation, but you said before that your goal is `finding out the 
pattern' and then you observed this. Now, I consider my moral (yes!) 
obligation to help clarifying these points, since I spent many months 
on these issues and many more I'm going to spend.

Actually, the underlying problem, and I'm sure you agree also on 
this, is understanding cut elimination in a uniform way for the 
vastest possible range of logics. This incredible uniformity we 
observe is *certainly* a key to the solution of this problem, one of 
the biggest in structural proof theory. So, we are talking about 
important things! There certainly are more important things in life, 
but this mailing list is for debating these sillier ones.

Anyway, I stop here, I feel like an old trombone and it's all your fault.

-Alessio