# Negative formula

A negative formula is a formula N such that $\wn N\limp N$ (thus a algebra for the monad $\wn$). As a consequence N and $\wn N$ are equivalent.

A formula N is negative if and only if $N\orth$ is positive.

## Negative connectives

A connective c of arity n is negative if for any negative formulas N1,...,Nn, $c(N_1,\dots,N_n)$ is negative.

Proposition (Negative connectives)

$\parr$, $\bot$, $\with$, $\top$, $\wn$ and $\forall$ are negative connectives.

Proof.  This is equivalent to the fact that $\tens$, $\one$, $\plus$, $\zero$, $\oc$ and $\exists$ are positive connectives.

More generally, $\wn A$ is negative for any formula A.

The notion of negative connective is related with but different from the notion of synchronous connective.

## Generalized structural rules

Negative formulas admit generalized right structural rules corresponding to a structure of $\parr$-monoid: $N\parr N\limp N$ and $\bot\limp N$. The following rule is derivable:

$\AxRule{\Gamma\vdash N,N,\Delta} \LabelRule{- c R} \UnaRule{\Gamma\vdash N,\Delta} \DisplayProof \qquad \AxRule{\Gamma\vdash\Delta} \LabelRule{- w R} \UnaRule{\Gamma\vdash N,\Delta} \DisplayProof$

Proof.  This is equivalent to the generalized left structural rules for positive formulas.

Negative formulas are also acceptable in the context of the promotion rule. The following rule is derivable:

$\AxRule{\vdash A,N_1,\dots,N_n} \LabelRule{- \oc R} \UnaRule{\vdash \oc{A},N_1,\dots,N_n} \DisplayProof$

Proof.  This is equivalent to the possibility of having positive formulas in the left-hand side context of the promotion rule.