E2. Building blocks of linear logic
The previous episode ended with a brief introduction to basic building blocks of linear logic, in particular, the ones that would allow creating compound statements from the smaller ones. In this episode, we shall have a closer look at them. Lets go!
Negation
Negation allows considering the not form of a statement, hence in a sense, its the dual of a statement. However, the not form, in general, does not mean the exact opposite. For example, the negation of a statement such as to spend a dollar is to receive a dollar (and not not spending a dollar). The negation of a statement such as to buy an apple is to sell an apple.
Negation switches perspectives: to spend a dollar is from the perspective of the buyer and to receive a dollar is from the perspective of the seller. Negation signifies the duality of perspectives in conversion of resources. Negation is an involution ; this means that double negation = no negation, .
The symbol for negation is (here, read as perp) for any statement .
Multiplicatives
The four connectives , , ⅋, and are called the multiplicatives. Multiplicatives allow simultaneous access to two or more resources.
Linearly distributive categories is the sub-logic generated by the multiplicatives presented in the language of category theory. This sub-logic is referred to in the literature as the "multiplicative linear logic (MLL)". Star autonomous categories is the sub-logic of the multiplicatives and the negation.
Dear Reader,
I would not be using ⅋ symbol anymore in this series, and have happily replaced it by . I have also replaced by , following the convention set in the original paper on linearly distributive categories (1997) by Cockett and Seely.
To all the critics of this change in notation, Cockett and Seely wrote in their sequel paper (1999), "More controversial perhaps is our insistence upon the use of for 'par' and for the coproduct 'sum'. As category theorists we are unrepentant upon this point, and there the matter must rest."
Let us see what these connectives mean intiutively. A statement, (read as A tensor B) allows the resources and to be available at the same time. For example, consider the following statements:
Then, refers to the fact that a dollar 💵 buys an apple 🍎 and an orange 🍊 at the same time.
The connective (read as top) which is the multiplicative truth is the unit of the tensor. Hence, (multiplying with a number gives back the number).
The connective (read as bot) is the multiplicative false. and are duals to one another, that is, . The connective, (read as the par) is dual to the tensor. This means that, . An intuitive interpretation of the par is more subtle. It is better understood by interpreting within a specific context.
Linearly distributive categories are the framework where the interplay of the tensor and the par along with their units is explained without the use of negation.
Exponentials
Exponentials allow for non-linear operations within the logic. Instead of one resource becoming the other exponentials allow resources to reproduce (without any check) and to disappear!
An infinte storage of apples is written as 🍎 (pronounced bang an apple, or of course an apple). From this storage, one can extract an apples any number of times. The storage of a resource itself can produce another copy of itself or can vanish in thin air! In category theory, these are modelled using coalgebra modalities (TODO: put link here) and have deep connections to differential categories (TODO: put link here).
There is another exponential modality, who is an hungry pacman. A 🍎 (pronounced whimper an apple, or why not an apple) is an ever-hungry hungry pacman for apple resource. Two such hungry pacmans can combine into one or can appear out of thin air.
Negation puts the infinite storage and the hungry pacman on the same pedestal: negating a hungry pacman for apples gives an infinite storage of negated apples (whatever that means!).
Fun fact: The term whimper was coined by Richard (Rick) Blute from University of Ottawa, one of the pioneers of linearly distributive categories.
Additives
I am going to skip these for now since they would not be reappearing on the stage in the immediate future.
In the next episode, we shall see how a wide range of categories from linearly distributive to monoidal, are simply the multiplicative fragment of linear logic with different constraints placed on the interplay of the tensor and the par! 🎉