Re: How to use `deep inference'?

Hello,

it's good to start the day at dawn with a fierce moral duel.

At 19:35 +0200 27.4.04, Lutz Strassburger wrote:
>On Tuesday 27 April 2004 15:49, Alessio Guglielmi wrote:
>>I mean, you're right from your point of view, but your point of 
>>view is morally wrong!
>
>No, you just gave a morally wrong interpretation of my point of view.

No, I insist that your point of view is morally wrong and your answer 
strengthens my opinion.

Before using my Hattori Hanzo sword, let me say that I guess we 
agree, as we always did, on all the technical matters. I also guess 
we agree that `morally right' means `that will bring new, interesting 
questions and results'.

>>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.
>
>It is the other way around. there are some rules in the non-core which follow
>the scheme, and some do not.

Let's agree that the scheme is hyperswitch/medial as in my note on 
subatomic stuff. In this case, all rules of classical logic and all 
thirty-something but one of linear logic obey it, plus many in modal 
logics and so on. I'm sure you agree on this because this is either a 
trivial observation or just a matter of doing a mechanical check.

That said, many more rules will fall outside of my scheme if you 
design them out of proper mathematical axioms, special inferences, 
fine tunings and pathologies, that's for granted. I guess you agree 
that nobody will ever manage to capture this infinite variety by a 
simple scheme. Only thing one can hope for is to have some clues 
about what to do for designing `good' rules in these cases; every day 
we learn more and more on this (see for example recent work by 
Charles, Phiniki and Robert).

>All I am trying to do now is to find out the pattern. What do we 
>observe? all rules that follow the recipe are derivable in the 
>system {c,w}, i.e. general contraction and weakening. And those 
>rules that do not follow the pattern cannot be replaced by a 
>derivation containing only contraction and weakening. It is just an 
>observation. no relation sequent calculus context treatment.

OK. This is where you're very, very wrong, morally.

You are saying that the rules that follow the `recipe' are derivable 
for contraction and weakening, and you are making a moral point out 
of this observation.

1) What is the `recipe'? The recipe is nothing else that an algorithm 
for generating rules in the `core'.

2) What is the `core' of a system? It is the set of inference rules 
which are necessary for reducing identity and cut to their atomic 
forms.

3) What is necessary for this reduction? It is necessary to perform a 
STRUCTURAL INDUCTION on formulae by way of sound inference rules. 
Observation: structural induction is hardly a surprising concept, 
what is more interesting is that you can perform it by only using 
sound rules.

4) The recipe for the core extends to the non-core in the medial 
scheme, where the same mechanism of STRUCTURAL INDUCTION is used for 
making contraction atomic (and many more wonderful things, of course).

 From 1), 2), 3) and 4) one concludes that the recipe is about making 
structural induction and what is surprising is that this can be done 
by sound rules. Since this is something that you cannot do in any 
other formalism except CoS, there certainly is some value in it.

Now, what use do you make of contraction and weakening? You just use 
them for performing a STRUCTURAL INDUCTION!! Going up in a 
derivation, contraction duplicates and then you use weakening in both 
`branches' to select what you need: structural induction.

So, what you are observing is just a mechanism that does structural 
induction on rules that are *already designed* for structural 
induction! And the point is that structural induction is a 
triviality. What is non-trivial is the fact that the rules that 
realise it are sound, but this crucial information is *lost* when you 
translate them into contraction+weakening.

Another problem you have is that this structural induction is not 
performed, as in the recipe, by very tight rules, but by two rules 
that are much too powerful, and that in fact break easily.

To see this, take classical logic in its atomic presentation, keep 
medial and throw away atomic contraction and weakening. You are left 
with a weird linear logic which includes medial, but where you cannot 
analyse medial with weakening and contraction simply because they are 
not sound any more.

But then, summarising: even if it worked (it doesn't): what would be 
the point in reducing everything to general contraction and 
weakening? Much of the battle we are fighting against bureaucracy is 
*against* these rules, especially contraction. The right moral 
viewpoint is the opposite: finding an *atomic* scheme with *no* 
sharing and duplication.

-Alessio