Positive formula

From LLWiki
(Difference between revisions)
Jump to: navigation, search
(Generalized structural rules)
m (Generalized structural rules: with \VdotsRule)
Line 174: Line 174:
 
{{Proof|
 
{{Proof|
 
<math>
 
<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{P_n\vdash\oc{P_n}}
 
\AxRule{\oc\Gamma,P_1,\dots,P_n\vdash A,\wn\Delta}
 
\AxRule{\oc\Gamma,P_1,\dots,P_n\vdash A,\wn\Delta}
 
\LabelRule{\oc L}
 
\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}
 
\LabelRule{\oc L}
 
\UnaRule{\oc\Gamma,\oc{P_1},\dots,\oc{P_n}\vdash A,\wn\Delta}
 
\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}
 
\UnaRule{\oc\Gamma,\oc{P_1},\dots,\oc{P_n}\vdash \oc{A},\wn\Delta}
 
\LabelRule{\rulename{cut}}
 
\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}}
 
\LabelRule{\rulename{cut}}
 
\BinRule{\oc\Gamma,P_1,\dots,P_n\vdash \oc{A},\wn\Delta}
 
\BinRule{\oc\Gamma,P_1,\dots,P_n\vdash \oc{A},\wn\Delta}

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 P1,...,Pn, 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

Personal tools