Re: How to use `deep inference'?

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.

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

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

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

Actually it is. But that is a different topic.

>
>    [Ex.R,Ex.T]
>    -----------
>     Ex.[R,T]
>
> about a contraction??

see above. you can replace it by one contraction and two weakenings.

-Lutz