# Positive formula

m (Updated the 'equivalent' link) |
(→Generalized structural rules) |
||

Line 174: | Line 174: | ||

{{Proof| |
{{Proof| |
||

<math> |
<math> |
||

− | \AxRule{P_1\vdash\oc{P_1}} |
+ | \AxRule{\begin{array}{c}\\P_1\vdash\oc{P_1}\end{array}} |

\AxRule{P_n\vdash\oc{P_n}} |
\AxRule{P_n\vdash\oc{P_n}} |
||

\AxRule{\oc\Gamma,P_1,\dots,P_n\vdash A,\wn\Delta} |
\AxRule{\oc\Gamma,P_1,\dots,P_n\vdash A,\wn\Delta} |
||

Line 185: | Line 185: | ||

\UnaRule{\oc\Gamma,\oc{P_1},\dots,\oc{P_n}\vdash \oc{A},\wn\Delta} |
\UnaRule{\oc\Gamma,\oc{P_1},\dots,\oc{P_n}\vdash \oc{A},\wn\Delta} |
||

\LabelRule{\rulename{cut}} |
\LabelRule{\rulename{cut}} |
||

− | \BinRule{\oc\Gamma,\oc{P_1},\dots,P_n\vdash \oc{A},\wn\Delta} |
+ | \BinRule{\begin{array}{c}\oc\Gamma,\oc{P_1},\dots,P_n\vdash \oc{A},\wn\Delta\\\vdots\end{array}} |

− | \UnaRule{\vdots} |
||

\LabelRule{\rulename{cut}} |
\LabelRule{\rulename{cut}} |
||

\BinRule{\oc\Gamma,P_1,\dots,P_n\vdash \oc{A},\wn\Delta} |
\BinRule{\oc\Gamma,P_1,\dots,P_n\vdash \oc{A},\wn\Delta} |

## Revision as of 15:55, 16 July 2009

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

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