# Positive formula

m (→Generalized structural rules: with \VdotsRule) |
m (→Generalized structural rules: Link to wikipedia:comoind) |
||

(One intermediate revision by one user not shown) | |||

Line 1: | Line 1: | ||

A ''positive formula'' is a formula <math>P</math> such that <math>P\limp\oc P</math> (thus a [[Wikipedia:F-coalgebra|coalgebra]] for the [[Wikipedia:Comonad|comonad]] <math>\oc</math>). As a consequence <math>P</math> and <math>\oc P</math> are [[Sequent calculus#Equivalences|equivalent]]. |
A ''positive formula'' is a formula <math>P</math> such that <math>P\limp\oc P</math> (thus a [[Wikipedia:F-coalgebra|coalgebra]] for the [[Wikipedia:Comonad|comonad]] <math>\oc</math>). As a consequence <math>P</math> and <math>\oc P</math> are [[Sequent calculus#Equivalences|equivalent]]. |
||

+ | |||

+ | A formula <math>P</math> is positive if and only if <math>P\orth</math> is [[Negative formula|negative]]. |
||

== Positive connectives == |
== Positive connectives == |
||

Line 121: | Line 123: | ||

== Generalized structural rules == |
== Generalized structural rules == |
||

− | Positive formulas admit generalized left structural rules corresponding to a structure of <math>\tens</math>-comonoid: <math>P\limp P\tens P</math> and <math>P\limp\one</math>. The following rule is derivable: |
+ | Positive formulas admit generalized left structural rules corresponding to a structure of [[Wikipedia:Comonoid|<math>\tens</math>-comonoid]]: <math>P\limp P\tens P</math> and <math>P\limp\one</math>. The following rule is derivable: |

<math> |
<math> |

## Latest revision as of 19:49, 28 October 2013

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

A formula *P* is positive if and only if is negative.

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

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