This post is the second in a series on Logic. These ideas are very useful in understanding many important papers on programming language theory, especially papers on type theory and the lambda calculus. The first post was an explanation of sequents and Sequent Calculus as a system for doing logic, so I'll assume that you have an understanding of those concepts now. In this post I'll dive into linear logic, as the most amazing result of studying the sequent calculus. I'll finish the trilogy in the next post, where I discuss Par and computational interpretations of classical logic.
(I'm going to be leaving every usage of the Exchange rule implicit in all proofs in this post, as is customary for linear logic. It may be helpful to know that they are actually still happening anyway, unwritten.)
In the last post we realized that sequent notation can give a fairly elegant characterization of intuitionistic logic: restricting the right side of the turnstile (\(\vdash\)) to having at most one expression. As pleasing as that is, it also costs us a lot of the beauty of the sequent calculus, namely the symmetry between the two sides of the turnstile. Recall that in a classical sequent calculus, \(p,q\vdash r,s\) is equivalent to \(p,q,\neg r,\neg s\vdash\) and also \(\vdash\neg p,\neg q,r,s\). Let's take a moment to recap why that is, as a warmup for getting comfortable with the notation again:
In a more basic logical notation we could write the first one (informally) as \((p\land q)\Rightarrow (r\lor s)\).
The second one would be \((p\land q\land\neg r\land\neg s)\Rightarrow\texttt{False}\), because an empty right side means there must be a contradiction on the left. If you're familiar with abstract algebra or monoids, this is also because \(\texttt{False}\) is the "unit" for disjunction. So we now have \(\neg(p\land q\land\neg r\land\neg s)\), which we can De-Morgan into \(\neg p\lor\neg q\lor r\lor s\). In classical logic, \(\neg p\lor q\) is equivalent to implication, so let's do a little reverse-De-Morganing to get it into that form: \(\neg(p\land q)\lor r\lor s\). Finally we have \(p\land q\Rightarrow r\lor s\). Every step in this translation was reversible, so we know the two forms are equivalent.
The third one follows a very similar process so I won't go in as much depth. \(\texttt{True}\) is the unit for conjunction, so we get \(\texttt{True}\Rightarrow(\neg p\lor\neg q\lor r\lor s)\) and I'm sure you can do the rest.
(If you've done your category theory reading then I'll leave an easter egg as a reward: moving negation across implication like this is because negation is self-adjoint, a property that gives rise to the double-negation monad used to model continuations! But all of this is waaay above the expected background knowledge for this series :)
Well now we can see how to move things back and forth between the two sides of the turnstile, which is kinda cool. This process is how we did the one-sided sequent calculus in the last post, which if you'll recall only worked for classical logic. Since intuitionistic logic requires always having at most one expression on the right side, none of that works. And this is related to the fact that negation in intuitionistic logic is kinda wonky, and loses the gorgeous dualities of classical logic.
Having run into fundamental inconveniences with intuitionistic logic, the most natural question to ask is "why do we even care about intuitionistic logic? Why not just use classical logic, with all those nice properties?" The big problem with classical logic is the Law of Excluded Middle, or LEM. This is the axiom that lets us assume \(p\lor\neg p\) for any proposition \(p\) at all. Or equivalently the Double-Negation Elimination law, or DNE, which says that a proof that \(\neg p\) is false is enough to prove that \(p\) is true (\(\neg(\neg p)\Rightarrow p\)). Both of these feel true enough, but they don't give any reason that \(p\) is true, beyond just the fact that it isn't false. In intuitionistic logic, you can look at a proof of something and determine exactly what makes that thing true, from the proof itself. Take the example where \(p\) is "this Turing machine halts on this input." The classical logician says, "clearly it either halts on the input or it doesn't, there's no third option, so \(p\lor\neg p\)." The intuitionist then points out, "you clearly believe that either \(p\) or \(\neg p\) is true, so you should be able to tell me which one!" There isn't a way to do this in general, of course: you end up just running the machine on the input, but you can't wait "forever" to see if it halts or not. Intuitionistic logic has a powered-up disjunction: you can only prove a disjunction when you know which side of it is true, so when given a disjunction it's always valid to ask which side of it is true. It's an awesome property that puts intuitionistic logic in correspondence with various mathematical objects like toposes, bounded lattices, cartesian closed categories, and of course the lambda calculus.
Great, so we find ourselves in a situation where both classical logic and intuitionistic logic have some fundamental annoyances. None of them are major problems, and people do serious work in both systems to this day, but if we somehow found a logic that solved all these problems then we'd know it's somehow more "fundamental" and "natural," aka it probably has benefits we can't predict until we find such a logic.
A French logician named Jean-Yves Girard had all of these thoughts, and decided to see if sequent calculus can help. If you want all that nice symmetry across the turnstile, then of course your system needs to be some kind of sequent calculus in the first place. So the trick is defining a sequent calculus with negation-based moves across the turnstile where disjunctions (and existentials) still have that nice property of "remembering" what specifically is true.
(The word for this is "constructive." The idea is the proofs are "constructed" from smaller proofs, never erasing them like classical logic does. Intuitionistic logic is definitely thought of as the "main" constructive logic, causing the two to get conflated. Girard even says on page 4 of his work that I'm about to talk about that "There is no constructive logic beyond intuitionistic logic." However, that very work introduces the first serious contender with intuitionistic logic in the space of constructive logics!)
So why is it, exactly, that limiting a classical sequent calculus to only ever have at most one expression on the right makes the system constructive? Girard realized that it's because this prevents any usage of the contraction structural rule on the right side: if you can't have two proofs of \(p\lor q\) on the right side, then you can't use contraction to remove the duplicate. So classical logic can have \(\Gamma\vdash p,q\), use \(\lor\)-Intro-R\({}_1\) (creating a disjunction that is true because of its left side) and \(\lor\)-Intro-R\({}_2\) (creating a disjunction that is true because of its right side) to get to \(\Gamma\vdash p\lor q,p\lor q\), and contraction to dispose of either one of the two, ending up with \(\Gamma\vdash p\lor q\). We could have disposed of either disjunction, and they each are "true" for different reasons, so even if we classically know that this disjunction is true, any evidence that it's true (via the right or left side) has been completely forgotten.
So Girard proposes that, if the goal of the at-most-one-expression restriction on the right is to disallow contraction in instances that would break constructivity, then we can remove the restriction by instead simply disallowing contraction completely. Now we have the nice symmetry once more, and in fact Girard presents his new logic in the style of the one-sided sequent I mentioned in the last post! Now, a new problem arises in the face of constructivity, however, which is that you can simply using weakening to introduce a disjunction, obviously without knowing which side is true (the disjunction doesn't even need to be true!). So Girard simply bans weakening as well. (This wasn't a problem before because right-weakening was only possible when the right was empty, which already means there's a contradiction on the left.) In Girard's own words, "Once Once we have recognized that the constructive features of intuitionistic logic come from the dumping of structural rules on a specific place in the sequents, we are ready to face the consequences of this remark: the limitation should be generalized to the other rooms, i.e., weakening and contraction disappear" (Girard 1987, p. 4).
This final system, classical logic minus weakening and contraction, completely constructive, is called Linear Logic. The main downside now is that, well, there's no weakening and there's no contraction. Expressions can't be duplicated or dropped, so everything must be used exactly once. Girard has a solution to this that I'll get to later. One really weird consequence of this is that linear logic has a notion of truth/validity that isn't "monotonic," meaning that the amount of information you have to work with doesn't just go up throughout the proof. A proposition you've proven become "unproven" once you use it, meaning you need a new proof of it to use it again.
The first two rules I'll present are as follows:
Unfortunately, one does not simply remove weakening and contraction. With them gone, there are multiple ways to interpret the introduction and elimination rules from the one-sided sequent I presented in the last post. Take the example of \(\land\)-Intro:
When we bring this from classical logic to linear logic, we have to look at that \(\Delta\) with new caution. Taken directly into linear logic, this rule says that the \(p\) and the \(q\) have to be in the exact collection of propositions in order to form a conjunction with them. This is a big ask in linear logic, now that we can't introduce or remove propositions to make the two collections match up! Perhaps we prefer the following rule instead? It's equivalent in classical logic, but very much not in linear logic.
This states what might feel a little more intuitive, namely that conjunction doesn't actually care at all about the rest of the collections. But it's limiting in its own way, because now, if \(\Gamma\) and \(\Delta\) are equal, then the conjunction is in a collection where everything is duplicated! With no ability to remove them, this can cause serious problems. For example, we can't even prove \(p\Rightarrow p\land p\), aka \(\vdash\neg p,p\land p\):
You can hopefully see that there's this \(\neg p\) left over at the bottom and no way to get rid of it. Or equivalently, we've proven \(p\Rightarrow(p\Rightarrow(p\land p))\), but not our goal.
Linear logic simply decides to keep both! \(\land\) ("and") disappears, replaced by \(\&\) ("with") and \(\otimes\) ("tensor"):
So now \(p\Rightarrow p\&p\) is a theorem but \(p\Rightarrow p\otimes p\) is not. Meanwhile, because \(\&\) does get rid of that extra \(\neg p\), \(p\Rightarrow(p\Rightarrow(p\&p))\) is not a theorem, but of course \(p\Rightarrow(p\Rightarrow(p\otimes p))\) is.
Intuitively, \(p\otimes q\) means you've got both a \(p\) and a \(q\), since you can (and must) use both. Meanwhile \(p\&q\) means you've got this kind of dual-purpose thing that you can (and must) use once as either a \(p\) or a \(q\), but it's not a disjunction because you get to choose which. So we have the nice expected theorem \(p\&q\Rightarrow p\), but we don't have \(p\otimes q\Rightarrow p).
We do all this same stuff with disjunction, because we also have two possible translations of the classical and intuitionistic \(\lor\) rules. Here's the direct translation:
This is a useful form of disjunction, to be sure. But remember that the comma also means disjunction, since we're on the right of the sequent. So this must also be valid:
The question is, are these the same disjunction? The answer is no, because once again the comma-based case has the two propositions kind of "sharing" \(\Delta\), while the first case gave a \(\Delta\) to each. In this world where we can't really massage \(\Delta\) into arbitrary shapes, this distinction matters quite a lot.
So linear logic takes both once more! \(\lor\) ("or") disappears, replaced with \(\oplus\) ("plus") and \(\unicode{8523}\) ("par"). Yes, par the namesake of this series!
\(p\Rightarrow p\otimes q\) is a theorem, but \(p\Rightarrow p\unicode{8523} q\) is not. Meanwhile \(p\Rightarrow(q\Rightarrow p\unicode{8523}q)\) is a theorem, but \(p\Rightarrow(q\Rightarrow p\oplus q)\) is not. So each is capturing different aspects of how we think about disjunction.
The very exciting thing here is that \(\unicode{8523}\) is coming from the classical disjunction (because it's the comma in a one-sided sequent calculus) and \(\otimes\) is coming from the intuitionistic disjunction (always introduced with either the left side or the right, without forgetting). So one exciting theorem of linear logic is \(p\unicode{8523}\neg p\), the law of the excluded middle!! In fact, recall that this is simply the Axiom rule:
In other words, the law of the excluded middle is simply \(p\Rightarrow p\), which is of course very constructively valid. Because, unlike in intuitionistic logic, implication is not its own operator, but simply defined (in one-sided sequent calculus style) as \(p\Rightarrow q=\neg p\unicode{8523} q\).
To respect the fact that implication here is simply defined, instead of being its own operator, we use a different symbol for it, \(\unicode{8888}\) ("lollipop"). This of course also behaves a little differently from intuitionistic implication, since proofs of it can't use contraction or weakening. I will be switching to the new symbol from now on.
I will have much more to say about par and classical disjunction in the next and final post, so I'm keeping it brief here. But there are two things worth mentioning. First, par is infamous for being very difficult to understand, and indeed it was the only operator that linear logic "discovered," since no prior logics had anything comparable. Second, once I did wrap my head around it, I found it to be the most beautiful logical operator ever, by far. Hence creating this massive series, pretty much just to bring par to the world :)
The only thing left now is linear logic's translation of negation. But guess what, linear logic simply defines negation in terms of other things as well! Negation is a function defined recursively as follows (the first two rules are for atoms):
The very important and awesome feature we see here is that negation is "involutive," meaning applying it twice cancels it out. So linear logic support double-negation elimination!
So we're done! We got all the operators! Right? Kind of, yes, but we're not done. Truth and falsity themselves have to be split into two versions each as well! \(\texttt{True}\) gets replaced with \(\top\) ("top") and \(1\) ("one"), and \(\texttt{False}\) gets replaced with \(\bot\) ("bottom") and \(0\) ("zero").
(there's no rule for introducing \(0\).)
Look at the ways these play with the sequent rules, and figure out what they do. The most I'll give you is a hint: in what situations do these four symbols contribute nothing? It's really worth thinking through this system for a little, maybe getting out the paper and pencil. If you get stuck, don't hesitate to reach out to me on any platform, and I'll try very thoroughly to help you through it :)
We need to extend the definition of negation for these new symbols as well:
Finally we've got some sort of complete system of linear logic here. In particular, this is called MALL, for "multiplicative-additive linear logic." That's because the \(\otimes\), \(\unicode{8523}\), \(1\), and \(\bot\) symbols are called the "multiplicative fragment" of linear logic (itself a complete logic called MLL), and the \(\&\), \(\oplus\), \(\top\), and \(0\) symbols are called the "additive fragment" (not really a standalone system because the linear logic right-comma is inherently multiplicative). The multiplicative fragment is generally classical in spirit, especially with how it treats disjunction and implication, whereas the additive fragment is more intuitionistic. I'll dig into this a bit more later in the post when I briefly discuss semantics.
But before that, there's one more addition to make. In order to reach the expressivity of intuitionistic or classical logic, we would love to have some (cautious) way of re-introducing weakening and contraction. That would truly give the best of all worlds! Girard's solution is two new operators, the "exponentials," \(!p\) ("of course \(p\)") and \(?p\) ("why not \(p\)"):
(\(?\Delta\) means a collection of propositions which all have \(?\) applied to them, like \(?p_0,?p_1,...,?p_n\).)
Since I'm following the original single-sided sequent calculus presentation, I'm focusing on the \(?\) exponential here. However it's worth mentioning that most presentations of linear logic you see nowadays are of "intuitionistic linear logic." This is a two-sided intuitionistic sequent calculus (at most one proposition on the right) without contraction or weakening, and it also does without par, \(\bot\), or \(?\) since they are generally only make sense with multiple propositions on the right. In the absence of these operators it also takes implication and negation as built-in "primitive" operators. ILL has a number of flaws compared to linear logic, but it's much easier to make sense of what's going on intuitively, since there's none of that mysterious par-business (or any of the multiple-propositions-on-the-right stuff that's equivalent to par). I say all of this because most presentations of linear logic focus on the \(!\) exponential instead of \(?\) since they've removed \(?\) and do much of their work on the left side of the sequent, where things are negated relative to the right, so (by the definition of negation) \(!\) on the left does all the things that \(?\) is doing in the above rules. We have no left side in this presentation, so we will see much less usage of \(!\) here.
This system is now called LL (the full linear logic), or also MAELL, since MELL (MLL plus exponentials) and MALL are also a viable systems, and adding the additive fragment to MELL or the exponentials to MALL both get you to LL, so LL = MAELL. This is also called "classical linear logic" or CLL, to differentiate it from the very-popular ILL I just mentioned.
It's hopefully clear that MAELL is as expressive as intuitionistic or classical logic (because of the E). However, the exponentials offer a way of tracking usage of contraction and weakening. Notice that there's no way in general to go from \(?p\) to \(p\), which means that any theorem that doesn't mention the exponentials must have a proof that doesn't use the exponentials! The problematic version of the law of excluded middle is \(p\oplus\neg p\), and LL still has no proof of this proposition, even with the exponentials. It does, however, have a proof of \(?(p\oplus\neg p)\), using the trick I mentioned in the introduction:
Notice that \(p\oplus\neg p\unicode{8523}p\oplus\neg p\) is a theorem of linear logic, where one \(\oplus\) ("additive disjunction") is true due to its left side and the other additive disjunction is true due to its right side. This is again because par ("multiplicative disjunction") is a constructive way of getting some of the behavior of classical disjunction. Notice how the contraction in the above proof removes one of these additive disjunctions, but we don't know which, thereby forgetting the evidence in the final additive disjunction. So, unsurprisingly, theorems that use exponentials aren't necessarily constructive. But again, since there's no way to get rid of an exponential once you have it, you always know that theorems of propositions that don't use exponentials have proofs that don't use exponentials, and are therefore completely constructive. This gives a much better guarantee than classical logic: instead of, as in classical logic, being generally uncertain about the constructivity of a theorem, proofs that use unconstructive reasoning in linear logic must "admit to it" in their conclusion!
(This is why the \(?\) introduction rule is called Dereliction instead of \(?\)-Intro: usage of this rule is an abandonment of constructivity! Restraining from using this rule is the very "spirit" of constructivity, and usage of the rule eliminates, by preservation of \(?\), any claim to constructivity in the final theorem.)
(One beautiful technical detail: you might think the Cut rule could be used to hide usage of an exponential, since it can potentially remove any proposition. However, a fun result about linear logic is the "cut elimination" theorem, meaning any proof that uses Cut is proving a theorem that has a proof that doesn't use Cut. In other words, Cut can be completely eliminated from LL without changing what can be proven. Cut elimination is often a gorgeous result for a logic, because the algorithm of removing Cuts from a proof (to get a Cut-free proof of the same theorem) corresponds directly to program execution in some functional language! And proves that the functional language isn't Turing-complete, because it's guaranteed to halt! In this case it's the same reason as STLC, if you're familiar with that.)
Linear logic can seem quite weird, because using propositions exactly once feels very far removed from how we do logic as humans. There are a few interpretations of this logic that are worth mentioning.
The first is the "resource interpretation," since this is the most popular. This is also the most closely-tied to ILL, and therefore relatively unappealing in this series, but it needs to be known anyway. The classic teaching example is a vending machine. Say we have five units of money \(M\) (a limited resource), a fact represented by the proposition \(M\otimes M\otimes M\otimes M\otimes M\). Say a drink (\(D\)) costs two units of money, a proposition written \(?((M\otimes M)\unicode{8888}D)\) (the \(?\) reflects the fact that we can buy from the machine an arbitrary number of times). In normal logic, the first proposition is equivalent to \(M\) and the second is equivalent to \(M\Rightarrow D\), so we could conclude \(D\) and it would be equivalent to \(D\land D\land D\land D\) (or as many repetitions as we want). But that's not actually a valid inference from these two propositions in the real world, because the most we could possibly buy is two drinks. Linear logic reflects this: You can get from \((M\otimes M\otimes M\otimes M\otimes M)\) to \((D\otimes M\otimes M\otimes M)\), and from there to \(D\otimes D\otimes M\), but now \(M\otimes M\) is not true (because we're now out of money) so we can't apply our implication any more, and the most we were able to get is two drinks. Intuitionistic and classical logic are "monotonic," meaning information can only increase during a proof (I mentioned this in the introduction), so they have no way to say that at one point you have enough money and then later in the proof this stops being a fact.
The resource interpretation is loved because it applies to that friendly ILL I mentioned. In fact, it's used to model program memory as a limited resource in Rust! The rules of the borrowchecker come from a combination of syntax sugar and the rules of linear logic, which I find quite exciting.
But in this series we love the spicy stuff. What the heck is par!? Obviously I'll dig into par quite a bit in the next post (the post dedicated to par), where I talk about a semantics based on program control flow. But I'll briefly give three more semantics for linear logic before I finish up.
One very simple one worth mentioning is *-autonomous ("star-autonomous") categories in category theory. I won't dig into that because it's a deep category-theoretic rabbit hole that I don't want to pollute the prerequisite-knowledge-of-this-post with, but it's still worth mentioning that the (arguably) most popular category-theoretic foundation of intuitionistic logic and the lambda calculus is intuitionistic linear logic with exponentials (instead of having contraction and weakening just ambiently/implicitly), and that monoidal categories (which include *-autonomous categories) are regularly used for situations without contraction or weakening.
A slightly less scary one is a game-theoretic semantics. Game semantics is a gorgeous discipline that I'll write about more someday. It sounds scary to the non-game-theorist, but it's actually very simple. I'll go through this example more slowly because it has such a scary-sounding name. We'll be using "Conway games;" let me explain the rules.
A game is a bunch of dots ("positions") with arrows ("moves") between them. There's a red player and a blue player, and each move is either red or blue. The game progresses from dot to dot, starting at some "root position," where the red player picks a red outgoing arrow from the current dot, progressing the game to the next dot, and the blue player picks a blue outgoing arrow from that dot, etc. The game therefore wanders around the graph like that. A player loses when it's their turn but the current dot has no outgoing arrows of their color. Simple, right?
Conway games pop up in lots of surprising places because they give a very nice theory of "dialogues," that is two entities having an interaction where the things they can do, the choices available to them, depend on "how the interaction has gone so far," meaning the current position in the Conway game and the outgoing arrows of their color at that position.
A "strategy" is a deterministic plan for how you'll respond to everything your opponent can possibly do throughout the game. Because you lose a Conway game by running out of moves, a "winning strategy" (one that will always win no matter what choices the opponent makes) means a strategy that will never put you in a position where you have no moves left. In other words, a winning strategy defines a response to everything the opponent could possibly do, so it's useful to think of winning strategies like program flowcharts.
The application to linear logic is that we can define operators that transform Conway games into other, related Conway games, namely operators that look an awful lot like LL operators. The most famous and philosophicaly insightful example is that negation is simply swapping the colors of all the arrows. The binary operators are various ways to play two games simultaneously; with \(\otimes\) you have to win at both, with \(\oplus\) you have to win at one, and the other two can be derived by knowing that negation is swapping colors. I won't give a formal definition in this post, but I quite liked this paper. We then have conway games that look like, say, \(C\otimes\neg D\), and we say that a proof of this as an LL proposition is a winning strategy of this as a Conway game.
Thus game semantics give us this lovely idea, called "polarity," that a proof is successfully defending against every rebuttal the world ("Opponent") throws at it. Specifically, the polarity is the "color" of the move: is the choice in next position up to your proof, or up to the adversarial Opponent trying to disprove it? The philosophical insight is that negating something means that the Opponent is trying to prove that thing, and your proof is trying to refute it! I will discuss this more in the next post, but I really love it as a philosophy of logic. For more on the beautiful philosophy, check out this Stanford Encyclopedia of Philosophy entry.
Game semantics, and the philosophy it suggests, also sets us up for our final and most infamous LL semantics of this post: parallelism!
In this setting, programs in a highly-parallel functional programming language act as proofs of LL propositions, which correspond to their types. \(A\unicode{8523}B\) is the type of expressions which are an expression of type \(A\) and an expression of type \(B\) running in parallel, hence the name "par!" These parallel processes interact with each other in a way that's reminiscent of the game semantics I mentioned: when a value is sent from one process to another, its type in one is the negation of its type in the other. For example, a process asking for a value of type \(A\) will use that value as at type \(A\) (of course), but to the outside world this request has type \(\neg A\), because it's not a value of type \(A\), but a place to put such a value. Programs use Cut to communicate: they take the request at type \(\neg A\) and their \(A\)-type value and smash them together with Cut, triggering the code that was requesting the \(A\) to execute using the provided value. Notice that the Cut rule has \(\vdash\neg p,\Delta\), which can be seen as \(\vdash p\unicode{8888}\Delta\), so Cut can be thought of as Modus Ponens, or function application. If you want to learn more about this line of work, I highly recommend this paper.
Thus ends the crash course on linear logic! Next up is the final post, digging into the semantics of multiplicative disjunction (par) much more deeply.
I have a wiki up for a much quicker reference to the ideas and operators of linear logic, here.
© 2024 Ryan Brewer.