Equivalent eXchange

The four binary operators for Linear Logic can be described by their logical sequents, or inference rules (shown above in the table). Note that in the rules for the operators, the operator appears below and not above the horizontal line. Thus the sequents can be considered in two ways: moving from top to bottom, the operator is introduced, and moving from bottom to top, the operator is eliminated. As operators are introduced the rules deduce a formula containing instances of them, and as operators are eliminated the rules construct a proof of that formula without them. Also note that in the sequents the symbols A and B denote formula in our logic, and the symbols Γ and Δ are finite (possibly empty) sequences of formulae (but the order of the formulae do not matter), called contexts.

The rule for the operator & (with), additive conjunction, says that if A obtains along with the context Γ, and if B obtains also along with Γ, then A & B obtains along with Γ.

The rule for the operator ⊕ (plus), additive disjunction, says that if A obtains along with the context Γ, or if B obtains along with Γ, then A ⊕ B obtains along with Γ.

The rule for the operator ⅋ (par), multiplicative disjunction, says that if the combination A,B obtains along with the context Γ, then A ⅋ B obtains along with Γ.

The rule for the operator ⊗ (tensor), multiplicative conjunction, says that if A obtains along with context Γ, and if B obtains along with context Δ, then A ⊗ B obtains along with the combined context Γ,Δ.

There are several immediate observations we can make about these rules.

First, note that for operators & and ⅋, they are reversible. That is, if one obtains A & B or A ⅋ B, then one knows exactly what the previous step had to be to introduce the operator. In contrast, ⊕ and ⊗ are not reversible. If one has A ⊕ B, one doesn’t know if we started with A or with B. If one has A ⊗ B, one doesn’t know what was the context of A or what was the context of B.

For this reason, I will consider & and ⅋ to be rational, and ⊕ and ⊗ to be empirical.

Second, note that all of the parts of the multiplicative sequents for ⅋ and ⊗ are the same above and below the horizontal line. In contrast, the parts of the additive sequents for & and ⊕ are different above and below the line. For &, a duplicated context is eliminated even as the operator is introduced. For ⊕, a new formula is introduced along with the introduction of the operator.

For this reason, I will consider & and ⊕ to be discrete, and ⅋ and ⊗ to be continuous.

References:

http://en.wikipedia.org/wiki/Sequent_calculus

http://en.wikipedia.org/wiki/Linear_logic

http://www.uni-obuda.hu/journal/Mihalyi_Novitzka_42.pdf

[*6.38, *6.40]

<>

This entry was posted on April 17, 2012 at 9:03 PM and is filed under fourfolds, linear logic, logic. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.