Talk:Intuitionistic linear logic
This is what used to be there.
Natural deduction formulation
editWe shall follow Martin Löf's style of hypothetical judgments. A linear hypothetical judgment , abbreviated as , defines the logical fact that the goal is obtained from the resources by consuming each resource exactly once. The simplest judgment is that of linear consumption of hypothesis, which is written as an axiomatic rule:
(Note that this is different from the usual hypothesis rule of ordinary logic, , because the sole allowed resource is the goal , 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 with a judgment having a linear resource .
substitution principle
editIf and , then .
The notation denotes multiset union.
Logical connectives
editThe connectives of ILL are of two major kinds: multiplicative and additive. Let us visit them in sequence.
Multiplicative conjunction
edit
Multiplicative implication
editI'll use to denote this connective, though the traditional glyph is \multimap
.
Multiplicative disjunction
editMultiplicative disjuntion or par is impossible in ILL.
Next the additive connectives.
Additive conjunction
editI 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)