Talk:Intuitionistic linear logic

This is what used to be there.

Natural deduction formulation

We shall follow Martin Löf's style of hypothetical judgments. A linear hypothetical judgment $A_{1},A_{2},\ldots ,A_{n}\vdash A$, abbreviated as $\Delta \vdash A$, defines the logical fact that the goal $A$ is obtained from the resources $A_{i}$ by consuming each resource exactly once. The simplest judgment is that of linear consumption of hypothesis, which is written as an axiomatic rule: ${\frac {}{A\vdash A}}$

(Note that this is different from the usual hypothesis rule of ordinary logic, ${\frac {}{\Gamma ,A\vdash A}}$, because the sole allowed resource is the goal $A$, which must be present; thus consumed exactly once.)

Dual to the hypothesis rule is a substitution principle that describes how to chain a judgment concluding $A$ with a judgment having a linear resource $A$.

substitution principle

If $\Delta \vdash A$ and $\Delta ',A\vdash C$, then $\Delta ,\Delta '\vdash C$.

The notation $\Delta ,\Delta '$ denotes multiset union.

Logical connectives

The connectives of ILL are of two major kinds: multiplicative and additive. Let us visit them in sequence.

Multiplicative conjunction

${\frac {\Delta \vdash A\quad \Delta '\vdash B}{\Delta ,\Delta '\vdash A\otimes B}}\otimes _{I}\qquad {\frac {\Delta \vdash A\otimes B\quad \Delta ',A,B\vdash C}{\Delta ,\Delta '\vdash C}}\otimes _{E}$

Multiplicative implication

I'll use $\rightarrow$ to denote this connective, though the traditional glyph is \multimap.

${\frac {\Delta ,A\vdash B}{\Delta \vdash A\rightarrow B}}\rightarrow _{I}\qquad {\frac {\Delta \vdash A\rightarrow B\quad \Delta '\vdash A}{\Delta ,\Delta '\vdash B}}\rightarrow _{E}$

Multiplicative disjunction

Multiplicative disjuntion or par is impossible in ILL.

Next the additive connectives.

Additive conjunction

I had to stop here because I can't for the life of me get the ampersand to work inside <math>. Time to upload images.

--Kaustuv Chaudhuri 07:22, 31 May 2004 (UTC)