2 Jun 2005 21:42

### A cut-free CoS system for S5

```Dear all,

attached is a paper (draft) I've written lately on the technical
results of my master thesis (completed last October in Dresden,
supervised by Charles Stewart). It is entitled "a system of deep
inference for the modal logic S5" and presents a cut-admissible system
for S5 in the calculus of structures. A short elaboration on the
importance and consequences of deep inference in modal systems is
given in the introduction.

I am planning to apply the final corrections/changes and submit it for
publication by the end of next week. Comments/suggestions/corrections
are more than welcome.

Regards,
Phiniki
```
Attachment (report_plain.pdf): application/pdf, 185 KiB
3 Jun 2005 10:27

### Paper announcement

```Dear All,

I would like to advertise the following paper, which is
accepted at the WoLLIC'05.

cheers,
-Ozan

Title: System BV is NP-complete

Abstract:
System BV is an extension of multiplicative linear logic
(MLL) with the rules mix, nullary mix, and a self-dual,
non-commutative logical operator, called seq. While the
rules mix and nullary mix extend the deductive system,
the operator seq extends the language of MLL. Due to the
operator seq, system BV extends the applications of MLL
to those where sequential composition is crucial, e.g.,
concurrency theory. System FBV is an extension of MLL
with the rules mix and nullary mix. In this paper, by
relying on the fact that system BV is a conservative
extension of system FBV, I show that system BV is
NP-complete by encoding the 3-Partition problem in FBV.
I provide a simple completeness proof of this encoding
by resorting to a novel proof theoretical method for
reducing the nondeterminism in proof search, which is
also of independent interest.

http://www.informatik.uni-leipzig.de/~ozan/Papers/BVnpc.pdf

```

3 Jun 2005 15:22

### New bureacracy/coherence

```Hi all,

I was investigating the simulation of LK cut-reduction in SKS (from a
semantic point of view)
and I came across the following pair of proofs (notation as in Lutz's
recent paper on proof nets and SKS):

[(A, f ) , (B,C)]
-----------------m
( [A,B] , [f, C])
----------------- up-t
( [A,B] , C)
----------------- s , plus some \sigmas
[ A , (B , C)]

and

[(A, f ) , (B,C)]
------------------- up-aw /down-aw (doesn't matter which, (it's coherent))
[(A, t ) , (B,C)]
--------------------- up-f
[ A , (B , C)]

Has anyone considered this kind of thing before?  The reason behind
considering the two
equal would be admissibilty of sequent calculus cut reduction in SKS
(specifically
reduction of cut against contraction).  It also looks like the kind of
coherence you might want to
hold of a categorical medial law.
```

3 Jun 2005 18:00

### Re: New bureacracy/coherence

```On Fri, 3 Jun 2005, Richard McKinley wrote:

> Hi all,
>
> I was investigating the simulation of LK cut-reduction in SKS (from a
> semantic point of view) and I came across the following pair of proofs
> (notation as in Lutz's recent paper on proof nets and SKS):
>
> [(A, f ) , (B,C)]
> -----------------m
> ( [A,B] , [f, C])
> ----------------- up-t
> ( [A,B] , C)
> ----------------- s , plus some \sigmas
> [ A , (B , C)]
>
>
> and
>
> [(A, f ) , (B,C)]
> ------------------- up-aw /down-aw (doesn't matter which, (it's coherent))
> [(A, t ) , (B,C)]
> --------------------- up-f
> [ A , (B , C)]
>
> Has anyone considered this kind of thing before?  The reason behind
> considering the two equal would be admissibilty of sequent calculus cut
> reduction in SKS (specifically reduction of cut against contraction).
> It also looks like the kind of coherence you might want to hold of a
> categorical medial law.
```

8 Jun 2005 11:46

### Re:New bureacracy/coherence

```At 2:22 PM +0100 3.6.05, Richard McKinley wrote:
>I was investigating the simulation of LK cut-reduction in SKS (from
>a semantic point of view) and I came across the following pair of
>proofs (notation as in Lutz's recent paper on proof nets and SKS):
>
>[(A, f ) , (B,C)]
>-----------------m
>( [A,B] , [f, C])
>----------------- up-t
>( [A,B] , C)
>----------------- s , plus some \sigmas
>[ A , (B , C)]
>
>
>and
>
>[(A, f ) , (B,C)]
>------------------- up-aw /down-aw (doesn't matter which, (it's coherent))
>[(A, t ) , (B,C)]
>--------------------- up-f
>[ A , (B , C)]
>
>Has anyone considered this kind of thing before?  The reason behind
>considering the two equal would be admissibilty of sequent calculus
>cut reduction in SKS (specifically reduction of cut against
>contraction).  It also looks like the kind of coherence you might
>want to hold of a categorical medial law.

Hi,

```

13 Jun 2005 06:36

### Re:A cut-free CoS system for S5

```At 21:42 +0200 2/6/05, Phiniki Stouppa wrote:
>attached is a paper (draft) I've written lately on the technical
>results of my master thesis (completed last October in Dresden,
>supervised by Charles Stewart). It is entitled "a system of deep
>inference for the modal logic S5" and presents a cut-admissible system
>for S5 in the calculus of structures. A short elaboration on the
>importance and consequences of deep inference in modal systems is
>given in the introduction.
>
>I am planning to apply the final corrections/changes and submit it for
>publication by the end of next week. Comments/suggestions/corrections
>are more than welcome.

Hello,

I'm sending you several comments privately. I have one issue which
could be suitable for discussion on the list.

The question is: Are the display calculus or hypersequents deep
inference formalisms? Should we consider them so?

As far as I know, people in these areas never considered themselves
as doing deep inference. Am I right? I think the term `deep
inference' has been invented by Kai, actually. If so, I'm not sure we
should tag the display calculus or hypersequents with deep inference,
at least in context where there isn't a thorough discussion.

I see the reasons for the modal logicians: there is a clear
indication that, in order to do proof theory for modal logic, there
is a need of *some form* of deep inference. This is clear.
```

13 Jun 2005 08:56

### Re:A cut-free CoS system for S5

```Ribbit all,

On Mon, 2005-06-13 at 14:36, Alessio Guglielmi wrote:
> The question is: Are the display calculus or hypersequents deep
> inference formalisms? Should we consider them so?

I don't know much about hypersequents but, from the little I know of
display calculus, I believe that it ought to be considered as a form of
deep inference. For instance, suppose we are working in a display
formalism and want to use a version of switch. Let's look at how to do
this on the left of the turnstile. What we want is a rule that says
something like (where | is "or" and "&" is and):

(R|U)&T |- XoY
---------------  (*)
(R&T)|U |- XoY

How to show that this is admissable? Well, suppose that we have a proof
of (R|U)&T. Let us unravel it:

R |- T*oX   U |- Y
-----------------
(R|U) |- *ToXoY
--------------
(R|U)oT |- XoY
--------------
(R|U)&T |- XoY

Now we can yank the proofs of R |- T*oX and U |- Y and travel by a
different path:
```

13 Jun 2005 08:38

### Re: A cut-free CoS system for S5

```I think I concur with Alessio on the matter of the characterisation
of Deep Inference as "fully deep" inference.

There's no doubt that even the classical sequent calculus can be seen
as an inference system that is somewhat deep: if you think of a
sequent of the form X |- Y as consisting of a conditional with a
conjunction in the antecedent and a disjunction in the antecedent,
then we can make inferences down to that depth.

Display logic presentations of modal or other substructural logics
allow inferences to go inside more, allowing for existential
operators (diamond, or fusion) in antecedent position and universal
operators (box, or arrow, or fission) in succedent position, together
with a dualising operator.  There's no doubt that this allows for
more depth, but it doesn't provide a structure in which formulas can
be /atomised/, and this is the difference when we compare with CoS.
A disjunction in antecedent position cannot be converted into
structure.  (Its inferential power is exhibited by branching in the
sequent derivation: another way that the difference with CoS
manifests itself.  Here hypersequents and display sequents are on the
side of the sequent calculus, and CoS stands apart.)

(I'm beginning to form some ideas of why both approaches have their
clear to me yet.)

I'd be interested to hear if my take on this is thought to be
idiosyncratic, or if it's a fair statement of the situation.

Best wishes,
```

13 Jun 2005 16:37

### Re: A cut-free CoS system for S5

```
Hi Alessio, hi amphimaniacs,

> I'm sending you several comments privately. I have one issue which
> could be suitable for discussion on the list.

> The question is: Are the display calculus or hypersequents deep
> inference formalisms? Should we consider them so?

The terminology I'm now favouring is distinguishing three kinds of
depth:
1. Surface inference: what you get with no-frills Gentzen sequent
systems: for LK-like systems this means you can swim about
outermost disjunctions and no deeper.  (Note that one can be less
deep even than this: ie. the Hilbert calculus, and Alessio has
suggested one may even be able to get cut-elimination result for
some such depthless inference systems).
2. Non-surface inference: able to perform inference deeper than this:
the hypersequent calculus is an example of this; the system for S5
allows you to freely act around disjunctions inside necessities
inside disjunctions, but no deeper.
3. True deep inference: there is no bound on the logical complexity
that you're able to move about in.  Hence display logic is truly
deep.

Display logic does have a catch, and the way I would put it is this:
in order to maintain the subformula property, it is necessary to
"freeze" formulae that are produced by logical (as opposed to
structural) inference rules.  This means that conjunction-like rules
force a separation of their premisses, and so the inference takes
```

14 Jun 2005 01:40

### Re: A cut-free CoS system for S5

```
I agree with Greg. Displaying is a type of deep inference. But it is
not the same. Also, to my knowledge, nowhere in the display literature
is there any mention of the idea of rewriting at any depth. This is
explicit in CoS and in the rewriting literature of course. I would
even argue that there are reasons why we might want to avoid deep
inference. That is, it should be derivable but not necessarily built
in from the start to make sure that our rules capture substitution
properly.

raj

```

Gmane