# Polarized linear logic

m (→Polarization: link to positive formula) |
m (link to generalized structural rules) |
||

Line 1: | Line 1: | ||

− | '''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. |
+ | '''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 [[Positive_formula#Generalized_structural_rules|extended]] to the whole class of so called ''negative'' formulae. |

== Polarization == |
== Polarization == |

## Latest revision as of 10:28, 5 October 2011

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

## [edit] Polarization

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

The dual operation extended to propositions exchanges the roles of connectors and reverses the polarity of formulae.

## [edit] 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 , where Γ is a multiset of negative formulae, and Δ is a *stoup* that contains at most one positive formula (though it may be empty).