page 3  (8 pages)
to previous section2
4to next section

1 Introduction

2 A Derivation of the D Rule

Heinrich Wansing's [Wan94] structural rule for the seriality axiom D: 2p ! 3p

is not very convincing because it does not fit neatly into the Display Logic

framework. According to Marcus Kracht's [Kra93] analysis we should be able

to translate the seriality axiom in the form > ! 3> into a structural rule of

CMDL. Kracht's translation gives:

(Kracht's D rule) ? ffl ?I ` Z

I ` Z

However, it was not obvious to us how to derive the D axiom from this rule, or

indeed, how to derive Wansing's rule for seriality:

(Wansing's D Rule) fflX ffi fflY ` ?I

X ` ?Y

Below we show how this can be done.

The following derivation shows that the correct form of the seriality rule is as

given at the left, with the derivation at the right:

(D)
ffl(X ffi ?Y ) ` ?I

X ` Y

ffl(X ffi ?Y ) ` ?I
(dp)
X ffi ?Y ` ffl ? I (dp)
? ffl ?I ffi X ` Y (dp)
? ffl ?I ` ?X ffi Y (Kracht's D rule)
I ` ?X ffi Y (dp)
I ffi X ` Y (I? `)
X ` Y

Now, in the presence of contraction and weakening on the left hand side we can