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]
<>
July 3, 2012 at 1:52 PM |
[…] 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 […]
August 21, 2012 at 9:00 PM |
[…] There are associations between the Curry-Howard Correspondence and the fourfolds of the Square of Opposition, Attraction and Repulsion, and of course Linear Logic. […]
November 5, 2012 at 2:14 PM |
[…] 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 […]
January 11, 2013 at 3:31 PM |
[…] 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 […]
March 5, 2013 at 5:13 PM |
[…] 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 […]
March 22, 2013 at 5:19 PM |
[…] 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. […]
February 1, 2014 at 11:34 AM |
[…] 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 […]
April 21, 2014 at 10:10 AM |
[…] 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! […]
September 1, 2014 at 10:57 AM |
[…] 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 […]
February 26, 2015 at 11:21 AM |
[…] 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 […]
December 9, 2017 at 10:40 AM |
[…] https://equivalentexchange.wordpress.com/2012/04/17/the-four-binary-operators-of-linear-logic/ […]
April 6, 2019 at 7:48 AM |
[…] https://equivalentexchange.blog/2012/04/17/the-four-binary-operators-of-linear-logic/ […]