Re: How to use `deep inference'?

On Wednesday 28 April 2004 07:39, Alessio Guglielmi wrote:
> Hello,
>
> it's good to start the day at dawn with a fierce moral duel.

then let me end the day by finishing it.

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

So, we agree on all points. Only that you are forcing me into a nitpicking 
discussion on `morally right'-ness, which is according to you definition not 
morally right, because it doesn't lead us anywhere. 

Btw. having a good sword doesn't mean being a good samurai.

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

As you said, we agree on everything.

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

No. I am just making the obervation (which is still morally right because we 
might get something out of it), but I am not making any point out of it. 
Neither a moral one, nor a nonmoral one.

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

As you and I said, we agree on everything. 
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.
And you are wasting your (and my) time writing long mails about structural 
induction. According to your definition, this is "morally wrong". So, let's 
stop the "morally wrong" discussion, and do the "morally right" things, like 
proving that P=NP. I go home now.

-Lutz