Internal and External Choice

This article or section needs more cowbell.

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.