# Positive formula

A *positive formula* is a formula *P* such that (thus a coalgebra for the comonad ). As a consequence *P* and are equivalent.

A formula *P* is positive if and only if is negative.

## Positive connectives

A connective *c* of arity *n* is *positive* if for any positive formulas *P*_{1},...,*P*_{n}, is positive.

**Proposition** (Positive connectives)

, , , , and are positive connectives.

*Proof.*

More generally, is positive for any formula *A*.

The notion of positive connective is related with but different from the notion of asynchronous connective.

## Generalized structural rules

Positive formulas admit generalized left structural rules corresponding to a structure of -comonoid: and . The following rule is derivable:

*Proof.*

Positive formulas are also acceptable in the left-hand side context of the promotion rule. The following rule is derivable:

*Proof.*