# Polarized linear logic

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

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

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