Intuitionistic linear logic

Revision as of 22:03, 7 January 2009

Intuitionistic Linear Logic ( $I L L$ ) is the intuitionnistic restriction of linear logic: the sequent calculus of $I L L$ is obtained from the two-sided sequent calculus of linear logic by constraining sequents to have exactly one formula on the right-hand side: $\Gamma\vdash A$ .

The connectives $\parr$ , $\bot$ and $\wn$ are not available anymore, but the linear implication $\limp$ is.

Sequent Calculus

$\LabelRule{\textit{ax}} \NulRule{A\vdash A} \DisplayProof \qquad \AxRule{\Gamma\vdash A} \AxRule{\Delta,A\vdash C} \LabelRule{\textit{cut}} \BinRule{\Gamma,\Delta\vdash C} \DisplayProof$

$\AxRule{\Gamma\vdash A} \AxRule{\Delta\vdash B} \LabelRule{\tens R} \BinRule{\Gamma,\Delta\vdash A\tens B} \DisplayProof \qquad \AxRule{\Gamma,A,B\vdash C} \LabelRule{\tens L} \UnaRule{\Gamma,A\tens B\vdash C} \DisplayProof \qquad \LabelRule{\one R} \NulRule{{}\vdash\one} \DisplayProof \qquad \AxRule{\Gamma\vdash C} \LabelRule{\one L} \UnaRule{\Gamma,\one\vdash C} \DisplayProof$

$\AxRule{\Gamma,A\vdash B} \LabelRule{\limp R} \UnaRule{\Gamma\vdash A\limp B} \DisplayProof \qquad \AxRule{\Gamma\vdash A} \AxRule{\Delta,B\vdash C} \LabelRule{\limp L} \BinRule{\Gamma,\Delta,A\limp B\vdash C} \DisplayProof$

$\AxRule{\Gamma\vdash A} \AxRule{\Gamma\vdash B} \LabelRule{\with R} \BinRule{\Gamma\vdash A\with B} \DisplayProof \qquad \AxRule{\Gamma,A\vdash C} \LabelRule{\with_1 L} \UnaRule{\Gamma,A\with B\vdash C} \DisplayProof \qquad \AxRule{\Gamma,B\vdash C} \LabelRule{\with_2 L} \UnaRule{\Gamma,A\with B\vdash C} \DisplayProof \qquad \LabelRule{\top R} \NulRule{\Gamma\vdash\top} \DisplayProof$

$\AxRule{\Gamma\vdash A} \LabelRule{\plus_1 R} \UnaRule{\Gamma\vdash A\plus B} \DisplayProof \qquad \AxRule{\Gamma\vdash B} \LabelRule{\plus_2 R} \UnaRule{\Gamma\vdash A\plus B} \DisplayProof \qquad \AxRule{\Gamma,A\vdash C} \AxRule{\Gamma,B\vdash C} \LabelRule{\plus L} \BinRule{\Gamma,A\plus B\vdash C} \DisplayProof \qquad \LabelRule{\zero L} \NulRule{\Gamma,\zero\vdash C} \DisplayProof$

$\AxRule{\oc{\Gamma}\vdash A} \LabelRule{\oc R} \UnaRule{\oc{\Gamma}\vdash\oc{A}} \DisplayProof \qquad \AxRule{\Gamma,A\vdash C} \LabelRule{\oc d L} \UnaRule{\Gamma,\oc{A}\vdash C} \DisplayProof \qquad \AxRule{\Gamma,\oc{A},\oc{A}\vdash C} \LabelRule{\oc c L} \UnaRule{\Gamma,\oc{A}\vdash C} \DisplayProof \qquad \AxRule{\Gamma\vdash C} \LabelRule{\oc w L} \UnaRule{\Gamma,\oc{A}\vdash C} \DisplayProof$

$\AxRule{\Gamma\vdash A} \LabelRule{\forall R} \UnaRule{\Gamma\vdash \forall\alpha A} \DisplayProof \qquad \AxRule{\Gamma,A[\tau/\alpha]\vdash C} \LabelRule{\forall L} \UnaRule{\Gamma,\forall\alpha A\vdash C} \DisplayProof \qquad \AxRule{\Gamma\vdash A[\tau/\alpha]} \LabelRule{\exists R} \UnaRule{\Gamma\vdash\exists\alpha A} \DisplayProof \qquad \AxRule{\Gamma,A\vdash C} \LabelRule{\exists L} \UnaRule{\Gamma,\exists\alpha A\vdash C} \DisplayProof$

with $α$ not free in $Γ, C$ in the rules $\forall R$ and $\exists L$ .

The intuitionistic fragment of linear logic

In order to characterize intuitionistic linear logic inside linear logic, we define the intuitionistic restriction of linear formulas:

$J ::= X \mid J\tens J \mid \one \mid J\limp J \mid J\with J \mid \top \mid J\plus J \mid \zero \mid \oc{J} \mid \forall\alpha J \mid \exists\alpha J$

$J L L$ is the fragment of linear logic obtained by restriction to intuitionistic formulas.

Theorem ( $J L L$ and $I L L$ )

$\Gamma\vdash A$ is provable in $I L L 1$ if and only if it is provable in $J L L 1$ .

Proof. The first direction is immediate since $I L L 1$ is included in $J L L 1$ .

For the second direction, we consider a cut-free proof of $\Gamma\vdash A$ in $J L L 1$ . We prove by induction on the length of such a proof that it belongs to $I L L 1$ .

This result is still valid with units from $I L L 1$ into $J L L 1$ . In the opposite direction, it holds with $\one$ but not anymore with $\top$ and $\zero$ . ${}\vdash((X\limp Y)\limp\zero)\limp(X\tens\top)$ is provable in $J L L 1$ :

$\LabelRule{\textit{ax}} \NulRule{X\vdash X} \LabelRule{\top R} \NulRule{{}\vdash Y,\top} \LabelRule{\tens R} \BinRule{X\vdash Y,X\tens\top} \LabelRule{\limp R} \UnaRule{{}\vdash X\limp Y,X\tens\top} \LabelRule{\zero L} \NulRule{\zero\vdash {}} \LabelRule{\limp L} \BinRule{(X\limp Y)\limp\zero\vdash X\tens\top} \LabelRule{\limp R} \UnaRule{{}\vdash((X\limp Y)\limp\zero)\limp(X\tens\top)} \DisplayProof$

but not in $I L L 1$ .

Intuitionistic linear logic

Revision as of 22:03, 7 January 2009

Sequent Calculus

The intuitionistic fragment of linear logic

Views

Personal tools

Navigation

Search

Tools