Internal and External Choice
Many beginning students of intuitionistic linear logic are confused by the difference between multiplicative conjunction (⊗), additive conjunction (&), and additive disjunction (⊕). This may be because intuitionistic propositional logic features only two "combining" connectives, conjunction and disjunction. The additional connectives arise from the linear nature of resources in linear logic and, specifically, the difference between internal and external choice.
Suppose that Karl Marx has fifty dollars. With that much money, Karl could buy a nice communist flag to wave, or he could buy a ticket to St. Petersburg, but he cannot do both --- for that, he would need one hundred dollars. As a good party member, Karl is very frugal with the resources of the state! There is a choice involved here, but where that choice is made can be important:
- If Karl makes the decision himself, this is said to be an external choice. Given the alternative, Karl can take the option he prefers.
- However, if Karl gives the money to Vladimir Ilyich to decide, then the result is an internal choice. Karl must be prepared for either a flag or a ticket; he cannot predict which one he will get. Choosing an alterantive at random, or following a procedure which is infeasible to completely analyze, are said to produce internal choices.
An additive disjunction features an internal choice. If Karl has the resource A ⊕ B, and Karl wishes to produce the resource C, then Karl must be able to produce C from whichever of A or B he receives. However, to produce A ⊕ B, Karl must merely be able to produce one or the other. For example, if Karl has a pear, Karl can produce (a pear ⊕ a stable capitalistic society) --- it's quite possible that an internal choice might feature something impossible!
An additive conjunction features an external choice. If Karl has the resource A & B, and Karl wishes to produce the resource C, then Karl must be able to produce either C from A or C from B --- he can use whichever one is more convenient for him and the state. However, to produce A & B from some resources Δ, Karl must be able to produce A from Δ and he must be able to produce B from Δ.
A multiplicative conjunction features no choice at all! If Karl has the resource A ⊗ B, Karl has both resources at the same time, and he can use them both to good effect. Of course, to produce A ⊗ B, Karl must be able to produce both simultaneously from the set of resources he has.
Classical linear logic also includes a multiplicative disjunction, which captures the idea of having multiple resources which must be used separately; this isn't really distinguishable from multiplicative conjunction in intuitionistic linear logic.
A crazed fool might wonder if this article is confused. "Shouldn't", such a simpleton might posit, "external choice refer to additive disjunction? After all, the choice is made externally to the user." This fallacy is, as fallacies are wont to be, wantonly, contemptibly, and even morally wrong. The choice is internal to the disjunction, as its semantics are purely its own, and so this article's terminology is, if there were a god, which there isn't, as should be well understood by the reader, well in keeping with the divine plan. No further comments will be entertaining.
Tea and Crumpets
Oh, please sit down! Right here on the divan! Can I get your coat? Think nothing of it! My, my, yes, help yourself. The family and I will now put on a performance of King Lear. We do hope the acting isn't too wooden.