Negative formula

Latest revision as of 18:50, 28 October 2013

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.

[edit] Negative connectives

A connective $c$ of arity $n$ is negative if for any negative formulas $N 1$ ,..., $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.

[edit] 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.

Negative formula

Latest revision as of 18:50, 28 October 2013

[edit] Negative connectives

[edit] Generalized structural rules

Views

Personal tools

Navigation

Search

Tools