# Sequentialized Empires and Kingdoms

Date: Thu, 21 Nov 91 14:19:38 GMT
To: linear@cs.stanford.edu

In response to Patrick Lincoln's note about the sequent calculus
analog of empires and kingdoms:

What you say about the empires coincides with a result of mine
in the paper "Proof Nets for MALL" (submitted to the Annals),
which holds for the whole propositional LL including exponentials
(provided that we agree on a discipline for the constants, e.g.,
apply/permute the \bottom rule-weakenings immediately after the axioms).
I use the notions of proof-nets for MALL and slicings as in a previous
message.
----------------------------------------------------------------------
There are maps
*                  star
Sequent Derivations   ---->  Proof Nets  ----> Families of Slices

with the following property:
(writing D^*, D^{*\ast}, but also A^* for A a formula-occurrence in D,
and also N^-*, etc.)

Theorem: Let D be any derivation of Gamma in propositional linear logic.
For every formula A occurring in D there exists a derivation D',
which is obtained from D by permuting the order of inferences,
with the following properties:

(1) Suppose A is introduced in D by either the \otimes rule or
the \par rule or by a Contraction with active formulas A_1 and A_2;
let B = A^*, B_1 = A_1^*, B_2 = A_2^*; then

(i) D^* = (D')^*;

(ii) in D', (e(B_1) U  e(B_2))^{-*} is the set of formula occurrences
that are introduced above A (= B^{-*}).

(2) Suppose A is introduced in D either by the \oplus rule or
by Weakening or Dereliction; let B = A^*; then

(i) D^* = (D')^*;

(ii) in D', (e(B))^{-*} is the set of formula occurrences that are
introduced above A (= B^{-*}).

(3) Suppose A is introduced in D by the \with rule; let B = A^*; then

(i) D^{*\star} = (D')^{*\star};

(ii) there is B' in D'^* such that (e(B))^star = (e(B'))^star and
in D', (e(B'))^{-*} is the set of formula occurrences that are
introduced above A (= B'^{-*}).
-----------------------------------------------------------------------
It seems reasonable that one should prove the corresponding result
for kingdoms.

I should say that nobody else has yet checked (3), although (1)
and (2) are established.

Gianluigi Bellin