Positive formula - Revision history

Olivier Laurent: /* Generalized structural rules */ Link to wikipedia:comoind

2013-10-28T17:49:42Z

‎Generalized structural rules: Link to wikipedia:comoind

Olivier Laurent: Added link to negative formulas

2013-10-28T17:43:54Z

Added link to negative formulas

Olivier Laurent: /* Generalized structural rules */ with \VdotsRule

2009-07-16T21:28:35Z

‎Generalized structural rules: with \VdotsRule

Damiano Mazza: /* Generalized structural rules */

2009-07-16T13:55:55Z

‎Generalized structural rules

Emmanuel Beffara: Updated the 'equivalent' link

2009-03-12T15:53:49Z

Updated the 'equivalent' link

Olivier Laurent: New page: A ''positive formula'' is a formula $P$ such that $P\limp\oc P$ (thus a coalgebra for the comonad $\oc$ ). A...

2009-03-06T14:58:53Z

New page: A ''positive formula'' is a formula <math>P</math> such that <math>P\limp\oc P</math> (thus a coalgebra for the comonad <math>\oc</math>). A...

New page

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 and definability|equivalent]].

== Positive connectives ==

A connective <math>c</math> of arity <math>n</math> is ''positive'' if for any positive formulas <math>P_1</math>,...,<math>P_n</math>, <math>c(P_1,\dots,P_n)</math> is positive.

{{Proposition|title=Positive connectives|
<math>\tens</math>, <math>\one</math>, <math>\plus</math>, <math>\zero</math>, <math>\oc</math> and <math>\exists</math> are positive connectives.
}}

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

 

<math>
\LabelRule{\one R}
\NulRule{\vdash\one}
\LabelRule{\oc R}
\UnaRule{\vdash\oc{\one}}
\LabelRule{\one L}
\UnaRule{\one\vdash\oc{\one}}
\DisplayProof
</math>

 

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

 

<math>
\LabelRule{\zero L}
\NulRule{\zero\vdash\oc{\zero}}
\DisplayProof
</math>

 

<math>
\LabelRule{\rulename{ax}}
\NulRule{\oc{P}\vdash\oc{P}}
\LabelRule{\oc R}
\UnaRule{\oc{P}\vdash\oc{\oc{P}}}
\DisplayProof
</math>

 

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

More generally, <math>\oc A</math> is positive for any formula <math>A</math>.

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 <math>\tens</math>-comonoid: <math>P\limp P\tens P</math> and <math>P\limp\one</math>. The following rule is derivable:

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

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

 

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

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

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

{{Proof|
<math>
\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{\vdots}
\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,P_n\vdash \oc{A},\wn\Delta}
\UnaRule{\vdots}
\LabelRule{\rulename{cut}}
\BinRule{\oc\Gamma,P_1,\dots,P_n\vdash \oc{A},\wn\Delta}
\DisplayProof
</math>
}}

← Older revision		Revision as of 17:43, 28 October 2013
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 ==

← Older revision		Revision as of 15:53, 12 March 2009
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 and definability\|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]].

	== Positive connectives ==		== Positive connectives ==

@@ Line 123: / Line 123: @@
 == 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>

@@ 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}
 \LabelRule{\rulename{cut}}
 \BinRule{\oc\Gamma,P_1,\dots,P_n\vdash \oc{A},\wn\Delta}