The Four Binary Operators of Linear Logic


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]

<>

Advertisements

10 Responses to “The Four Binary Operators of Linear Logic”

  1. Structure-Function « Equivalent eXchange Says:

    […] a completely naturalistic fourfold operating for all things. This new version was inspired by the Four Operators of Linear Logic. Structure and function are commonplace terms in scientific discourse, and I wish to replace formal […]

  2. The Curry-Howard Correspondence « Equivalent eXchange Says:

    […] There are associations between the Curry-Howard Correspondence and the fourfolds of the Square of Opposition, Attraction and Repulsion, and of course Linear Logic. […]

  3. Fourfolds and Double Duals « Equivalent eXchange Says:

    […] reasons, I believe that the best exemplar for these fourfolds is the recent logical system known as Linear Logic, which has two combining binary operators and two dividing binary […]

  4. Schrödinger’s Cat « Equivalent eXchange Says:

    […] a certain way of being, but that is mostly what the Copenhagen Interpretation is saying. Indeed, Linear Logic, which has been described many times on this blog, has been used to describe aspects of quantum […]

  5. My Dear Aunt Sally | Equivalent eXchange Says:

    […] and even obsolete rule? Note the similarity between these four binary arithmetic operators and the four binary linear logic operators. In each there are two operators for combining: addition and multiplication in arithmetic, and the […]

  6. The Four Treasures, Part 2 | Equivalent eXchange Says:

    […] A specific legendary stone is one of the Four Treasures of Ireland. The other treasures are a special spear, an esteemed sword, and a distinguished cauldron, all whose unique qualities will not be described. But consider the general features of each item in relation to the Archic Matrix and the four operators of Linear Logic. […]

  7. Relations all the Way Down | Equivalent eXchange Says:

    […] from four basic relations, instead of four basic things? If so, could they be something like the four binary operators of linear logic? I have likened these four basic operators of Linear Logic to my fourfold Structure-Function, where […]

  8. Fourfolds and Double Duals, Part 2 | Equivalent eXchange Says:

    […] Also: a c & t’s mouth and c ⅋ t’s eye; a d ⊕ g’s nose and d ⊗ g’s eye. These are the binary operators of Linear Logic! […]

  9. Four Dimensional Space-time | Equivalent eXchange Says:

    […] another interesting comparison to this fourfold is to that of linear logic. One observation is that length and width can be considered reversible but depth and time can be […]

  10. The Rational Structure of Inquiring Systems | Equivalent eXchange Says:

    […] the Literal. My assignments match the conjunctive and disjunctive properties of the operators of Linear Logic. Also left out is the Universal and how it supersedes the Actual as we make a complete turn. I like […]

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s


%d bloggers like this: