View source for Polarized linear logic

'''Polarized linear logic''' (LLP) is a logic close to plain linear logic in which structural rules, usually restricted to <math>\wn</math>-formulas, have been extended to the whole class of so called ''negative'' formulae.

== Polarization ==

LLP relies on the notion of ''polarization'', that is, it discriminates between two types of formulae, ''negative'' (noted <math>M, N...</math>) vs. ''positive'' (<math>P, Q...</math>). They are mutually defined as follows:

<math>M, N ::= X \mid M \parr N \mid \bot \mid M \with N \mid \top \mid \wn{P}</math>

<math>P, Q ::= X\orth \mid P \otimes Q \mid 1 \mid P \oplus Q \mid 0 \mid \oc{N}</math>

The dual operation <math>(-)\orth</math> extended to propositions exchanges the roles of connectors and reverses the polarity of formulae.

== Deduction rules ==

They are several design choices for the structure of sequents. In particular, LLP proofs are ''focalized'', i.e. they contain at most one positive formula. We choose to represent this explicitly using sequents of the form <math>\vdash\Gamma\mid\Delta</math>, where <math>\Gamma</math> is a multiset of negative formulae, and <math>\Delta</math> is a ''stoup'' that contains at most one positive formula (though it may be empty).

<math>
\LabelRule{\rulename{ax}}
\NulRule{\vdash P\orth \mid P}
\DisplayProof
\qquad
\AxRule{\vdash \Gamma_1, N \mid \Delta}
\AxRule{\vdash \Gamma_2 \mid N\orth}
\LabelRule{\rulename{cut}}
\BinRule{\vdash\Gamma_1, \Gamma_2 \mid \Delta}
\DisplayProof
</math>

<br/>

<math>
\AxRule{\vdash\Gamma, N\mid\cdot}
\LabelRule{p}
\UnaRule{\vdash\Gamma\mid \oc{N}}
\DisplayProof
\qquad
\AxRule{\vdash\Gamma\mid P}
\LabelRule{d}
\UnaRule{\vdash\Gamma,\wn{P}\mid \cdot}
\DisplayProof
\qquad
\AxRule{\vdash\Gamma,N,N\mid \Delta}
\LabelRule{c}
\UnaRule{\vdash\Gamma, N\mid\Delta}
\DisplayProof
\qquad
\AxRule{\vdash\Gamma\mid \Delta}
\LabelRule{w}
\UnaRule{\vdash\Gamma,N\mid\Delta}
\DisplayProof
</math>

<br/>

<math>
\AxRule{\vdash\Gamma_1\mid P}
\AxRule{\vdash\Gamma_2\mid Q}
\LabelRule{\tens}
\BinRule{\vdash\Gamma_1,\Gamma_2\mid P\otimes Q}
\DisplayProof
\qquad
\LabelRule{\one}
\NulRule{\vdash\cdot\mid\one}
\DisplayProof
\qquad
\AxRule{\vdash\Gamma, M, N\mid \Delta}
\LabelRule{\parr}
\UnaRule{\vdash\Gamma, M\parr N\mid \Delta}
\DisplayProof
\qquad
\AxRule{\vdash\Gamma\mid \Delta}
\LabelRule{\bot}
\UnaRule{\vdash\Gamma, \bot\mid\Delta}
\DisplayProof
</math>

<br/>

<math>
\AxRule{\vdash\Gamma\mid P}
\LabelRule{\plus_1}
\UnaRule{\vdash\Gamma\mid P\plus Q}
\DisplayProof
\qquad
\AxRule{\vdash\Gamma\mid Q}
\LabelRule{\plus_2}
\UnaRule{\vdash\Gamma\mid P\plus Q}
\DisplayProof
\qquad
\AxRule{\vdash\Gamma,M\mid \Delta}
\AxRule{\vdash\Gamma,N\mid \Delta}
\LabelRule{\with}
\BinRule{\vdash\Gamma,M\with N\mid \Delta}
\DisplayProof
\qquad
\LabelRule{\top}
\NulRule{\vdash\Gamma,\top\mid \Delta}
\DisplayProof
</math>