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 N₁,...,N_n, $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.