
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