Positive formula

Revision as of 22:28, 16 July 2009

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

Positive connectives

A connective $c$ of arity $n$ is positive if for any positive formulas $P 1$ ,..., $P n$ , $c(P_1,\dots,P_n)$ is positive.

Proposition (Positive connectives)

$\tens$ , $\one$ , $\plus$ , $\zero$ , $\oc$ and $\exists$ are positive connectives.

Proof. $\AxRule{P_2\vdash\oc{P_2}} \AxRule{P_1\vdash\oc{P_1}} \LabelRule{\rulename{ax}} \NulRule{P_1\vdash P_1} \LabelRule{\rulename{ax}} \NulRule{P_2\vdash P_2} \LabelRule{\tens R} \BinRule{P_1,P_2\vdash P_1\tens P_2} \LabelRule{\oc d L} \UnaRule{\oc{P_1},P_2\vdash P_1\tens P_2} \LabelRule{\oc d L} \UnaRule{\oc{P_1},\oc{P_2}\vdash P_1\tens P_2} \LabelRule{\oc R} \UnaRule{\oc{P_1},\oc{P_2}\vdash\oc{(P_1\tens P_2)}} \LabelRule{\rulename{cut}} \BinRule{P_1,\oc{P_2}\vdash\oc{(P_1\tens P_2)}} \LabelRule{\rulename{cut}} \BinRule{P_1,P_2\vdash\oc{(P_1\tens P_2)}} \LabelRule{\tens L} \UnaRule{P_1\tens P_2\vdash\oc{(P_1\tens P_2)}} \DisplayProof$

$\LabelRule{\one R} \NulRule{\vdash\one} \LabelRule{\oc R} \UnaRule{\vdash\oc{\one}} \LabelRule{\one L} \UnaRule{\one\vdash\oc{\one}} \DisplayProof$

$\AxRule{P_1\vdash\oc{P_1}} \LabelRule{\rulename{ax}} \NulRule{P_1\vdash P_1} \LabelRule{\plus_1 R} \UnaRule{P_1\vdash P_1\plus P_2} \LabelRule{\oc d L} \UnaRule{\oc{P_1}\vdash P_1\plus P_2} \LabelRule{\oc R} \UnaRule{\oc{P_1}\vdash\oc{(P_1\plus P_2)}} \LabelRule{\rulename{cut}} \BinRule{P_1\vdash\oc{(P_1\plus P_2)}} \AxRule{P_2\vdash\oc{P_2}} \LabelRule{\rulename{ax}} \NulRule{P_2\vdash P_2} \LabelRule{\plus_2 R} \UnaRule{P_2\vdash P_1\plus P_2} \LabelRule{\oc d L} \UnaRule{\oc{P_2}\vdash P_1\plus P_2} \LabelRule{\oc R} \UnaRule{\oc{P_2}\vdash\oc{(P_1\plus P_2)}} \LabelRule{\rulename{cut}} \BinRule{P_2\vdash\oc{(P_1\plus P_2)}} \LabelRule{\plus L} \BinRule{P_1\plus P_2\vdash\oc{(P_1\plus P_2)}} \DisplayProof$

$\LabelRule{\zero L} \NulRule{\zero\vdash\oc{\zero}} \DisplayProof$

$\LabelRule{\rulename{ax}} \NulRule{\oc{P}\vdash\oc{P}} \LabelRule{\oc R} \UnaRule{\oc{P}\vdash\oc{\oc{P}}} \DisplayProof$

$\AxRule{P\vdash\oc{P}} \LabelRule{\rulename{ax}} \NulRule{P\vdash P} \LabelRule{\exists R} \UnaRule{P\vdash \exists\xi P} \LabelRule{\oc d L} \UnaRule{\oc{P}\vdash \exists\xi P} \LabelRule{\oc R} \UnaRule{\oc{P}\vdash\oc{\exists\xi P}} \LabelRule{\rulename{cut}} \BinRule{P\vdash\oc{\exists\xi P}} \LabelRule{\exists L} \UnaRule{\exists\xi P\vdash\oc{\exists\xi P}} \DisplayProof$

More generally, $\oc A$ is positive for any formula $A$ .

The notion of positive connective is related with but different from the notion of asynchronous connective.

Generalized structural rules

Positive formulas admit generalized left structural rules corresponding to a structure of $\tens$ -comonoid: $P\limp P\tens P$ and $P\limp\one$ . The following rule is derivable:

$\AxRule{\Gamma,P,P\vdash\Delta} \LabelRule{+ c L} \UnaRule{\Gamma,P\vdash\Delta} \DisplayProof \qquad \AxRule{\Gamma\vdash\Delta} \LabelRule{+ w L} \UnaRule{\Gamma,P\vdash\Delta} \DisplayProof$

Proof. $\AxRule{P\vdash\oc{P}} \AxRule{\Gamma,P,P\vdash\Delta} \LabelRule{\oc L} \UnaRule{\Gamma,P,\oc P\vdash\Delta} \LabelRule{\oc L} \UnaRule{\Gamma,\oc P,\oc P\vdash\Delta} \LabelRule{\oc c L} \UnaRule{\Gamma,\oc P\vdash\Delta} \LabelRule{\rulename{cut}} \BinRule{\Gamma,P\vdash\Delta} \DisplayProof$

$\AxRule{P\vdash\oc{P}} \AxRule{\Gamma\vdash\Delta} \LabelRule{\oc w L} \UnaRule{\Gamma,\oc P\vdash\Delta} \LabelRule{\rulename{cut}} \BinRule{\Gamma,P\vdash\Delta} \DisplayProof$

Positive formulas are also acceptable in the left-hand side context of the promotion rule. The following rule is derivable:

$\AxRule{\oc\Gamma,P_1,\dots,P_n\vdash A,\wn\Delta} \LabelRule{+ \oc R} \UnaRule{\oc\Gamma,P_1,\dots,P_n\vdash \oc{A},\wn\Delta} \DisplayProof$

Proof. $\AxRule{P_1\vdash\oc{P_1}} \AxRule{P_n\vdash\oc{P_n}} \AxRule{\oc\Gamma,P_1,\dots,P_n\vdash A,\wn\Delta} \LabelRule{\oc L} \UnaRule{\oc\Gamma,P_1,\dots,P_{n-1},\oc{P_n}\vdash A,\wn\Delta} \VdotsRule{}{\oc\Gamma,P_1,\oc{P_2},\dots,\oc{P_n}\vdash A,\wn\Delta} \LabelRule{\oc L} \UnaRule{\oc\Gamma,\oc{P_1},\dots,\oc{P_n}\vdash A,\wn\Delta} \LabelRule{\oc R} \UnaRule{\oc\Gamma,\oc{P_1},\dots,\oc{P_n}\vdash \oc{A},\wn\Delta} \LabelRule{\rulename{cut}} \BinRule{\oc\Gamma,\oc{P_1},\dots,\oc{P_{n-1}},P_n\vdash \oc{A},\wn\Delta} \VdotsRule{}{\oc\Gamma,\oc{P_1},P_2,\dots,P_n\vdash \oc{A},\wn\Delta} \LabelRule{\rulename{cut}} \BinRule{\oc\Gamma,P_1,\dots,P_n\vdash \oc{A},\wn\Delta} \DisplayProof$

Positive formula

Revision as of 22:28, 16 July 2009

Positive connectives

Generalized structural rules

Views

Personal tools

Navigation

Search

Tools

@@ Line 174: / Line 174: @@
 {{Proof|
 <math>
-\AxRule{\begin{array}{c}\\P_1\vdash\oc{P_1}\end{array}}
+\AxRule{P_1\vdash\oc{P_1}}
 \AxRule{P_n\vdash\oc{P_n}}
 \AxRule{\oc\Gamma,P_1,\dots,P_n\vdash A,\wn\Delta}
 \LabelRule{\oc L}
-\UnaRule{\oc\Gamma,P_1,\dots,\oc{P_n}\vdash A,\wn\Delta}
+\UnaRule{\oc\Gamma,P_1,\dots,P_{n-1},\oc{P_n}\vdash A,\wn\Delta}
-\UnaRule{\vdots}
+\VdotsRule{}{\oc\Gamma,P_1,\oc{P_2},\dots,\oc{P_n}\vdash A,\wn\Delta}
 \LabelRule{\oc L}
 \UnaRule{\oc\Gamma,\oc{P_1},\dots,\oc{P_n}\vdash A,\wn\Delta}
@@ Line 185: / Line 185: @@
 \UnaRule{\oc\Gamma,\oc{P_1},\dots,\oc{P_n}\vdash \oc{A},\wn\Delta}
 \LabelRule{\rulename{cut}}
-\BinRule{\begin{array}{c}\oc\Gamma,\oc{P_1},\dots,P_n\vdash \oc{A},\wn\Delta\\\vdots\end{array}}
+\BinRule{\oc\Gamma,\oc{P_1},\dots,\oc{P_{n-1}},P_n\vdash \oc{A},\wn\Delta}
+\VdotsRule{}{\oc\Gamma,\oc{P_1},P_2,\dots,P_n\vdash \oc{A},\wn\Delta}
 \LabelRule{\rulename{cut}}
 \BinRule{\oc\Gamma,P_1,\dots,P_n\vdash \oc{A},\wn\Delta}