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,\dots ,A_n⊢A$, abbreviated as $\mathrm{\Delta }⊢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⊢A}$

(Note that this is different from the usual hypothesis rule of ordinary logic, $\frac{}{\mathrm{\Gamma },A⊢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 $\mathrm{\Delta }⊢A$ and ${\mathrm{\Delta }}^{\prime },A⊢C$, then $\mathrm{\Delta },{\mathrm{\Delta }}^{\prime }⊢C$.

The notation $\mathrm{\Delta },{\mathrm{\Delta }}^{\prime }$ 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{\mathrm{\Delta }⊢A{\mathrm{\Delta }}^{\prime }⊢B}{\mathrm{\Delta },{\mathrm{\Delta }}^{\prime }⊢A\otimes B}{\otimes }_I\frac{\mathrm{\Delta }⊢A\otimes B{\mathrm{\Delta }}^{\prime },A,B⊢C}{\mathrm{\Delta },{\mathrm{\Delta }}^{\prime }⊢C}{\otimes }_E$

Multiplicative implication

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

$\frac{\mathrm{\Delta },A⊢B}{\mathrm{\Delta }⊢A\to B}{\to }_I\frac{\mathrm{\Delta }⊢A\to B{\mathrm{\Delta }}^{\prime }⊢A}{\mathrm{\Delta },{\mathrm{\Delta }}^{\prime }⊢B}{\to }_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)