Exponentials in linear logic

The exponentials usually are introduced in one of the following
two ways:

1) Natural deduction style rules for !, then ? is defined by duality.

2) Sequent style rules for ! and ?. There are two rules, which
   contain both ! and ?. These rules may be used to prove, that
   ! and ? are dual to each other.
I would like to know, whether there exists an axiomatization of ! and ?
where every rule contains only ! or (i.e. XOR) ? and I would like
to know, how to prove duality of ! and ? then.

The main problem is as follows:

The rule !S contains ! and ?. It is

   ! \Gamma |- A, ? \Sigma
   ! \Gamma |- !A, ? \Sigma
If you know, that ! and ? are dual, you may transform this rule into
a rule of the following form

   ! \Gamma |- A
   ! \Gamma |- !A

by shifting all sequent elements of \Sigma from the right of |- to the left,
applying duality of ! and ? and adding them to the ! \Gamma block.

Similarly we can do with ?S.

Then we end up with a total of 8 formulae (!W, !D, !C, ?W, ?D, ?C and our
two modified !S and ?S).

However I am not aware, how we can show that ! and ? are dual using these
8 formulae.


Please answer to cap@ifi.unizh.ch

* Prof. Clemens H. CAP              cap@ifi.unizh.ch               (email)
* Dept. of Computer Science         +41-1-257 / 4326, 4331  (office voice)
* University of Zurich              +41-1-363 00 35           (office fax)
* Winterthurerstr. 190              +41-1-362 97 11  (home; voice and fax)
* CH-8057 Zurich, Switzerland 
* Motto: "Please do not read the last line of this signature".