[Prev][Next][Index][Thread]
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.
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".