Olivier Laurent: Dual version of positive formula

2013-10-28T17:50:07Z

New page

A ''negative formula'' is a formula <math>N</math> such that <math>\wn N\limp N</math> (thus a [[Wikipedia:F-algebra|algebra]] for the [[Wikipedia:Monad (category theory)|monad]] <math>\wn</math>). As a consequence <math>N</math> and <math>\wn N</math> are [[Sequent calculus#Equivalences|equivalent]].

A formula <math>N</math> is negative if and only if <math>N\orth</math> is [[Positive formula|positive]].

== Negative connectives ==

A connective <math>c</math> of arity <math>n</math> is ''negative'' if for any negative formulas <math>N_1</math>,...,<math>N_n</math>, <math>c(N_1,\dots,N_n)</math> is negative.

{{Proposition|title=Negative connectives|
<math>\parr</math>, <math>\bot</math>, <math>\with</math>, <math>\top</math>, <math>\wn</math> and <math>\forall</math> are negative connectives.
}}

{{Proof|
This is equivalent to the fact that <math>\tens</math>, <math>\one</math>, <math>\plus</math>, <math>\zero</math>, <math>\oc</math> and <math>\exists</math> are [[Positive formula#Positive connectives|positive connectives]].
}}

More generally, <math>\wn A</math> is negative for any formula <math>A</math>.

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 [[Wikipedia:Monoid (category theory)|<math>\parr</math>-monoid]]: <math>N\parr N\limp N</math> and <math>\bot\limp N</math>. The following rule is derivable:

<math>
\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
</math>

{{Proof|
This is equivalent to the [[Positive formula#Generalized structural rules|generalized left structural rules]] for positive formulas.
}}

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

<math>
\AxRule{\vdash A,N_1,\dots,N_n}
\LabelRule{- \oc R}
\UnaRule{\vdash \oc{A},N_1,\dots,N_n}
\DisplayProof
</math>

{{Proof|
This is equivalent to the possibility of having positive formulas in the [[Positive formula#Generalized structural rules|left-hand side context of the promotion rule]].
}}

Negative formula - Revision history

Olivier Laurent: Dual version of positive formula