# 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.

ANY HELP IS APPRECIATED, I WILL SUMMARIZE.