TL;DR: I want to know how linear logic works. Sorry for the long question, I try to explain myself as best as I can in hopes of receiving good answers, especially because I don't know anyone else to ask and it seems to be hard to find resources about this topic, e.g. there are just a handful of questions about LL on this site.
I'm very interested in proof search, therefore in proof nets, and thus I'm trying to understand linear logic. My goal is to be able to read this site and understand it.
I have never learned anything of this in university; I taught myself everything during plenty of (sometimes frustrating, sometimes interesting) hours. The introductions I read state that linear logic somehow limits the use of formulas in proofs to useful applications and I would like to understand how that works.
First I taught myself sequent calculus for classical logic, which already has some weird properties: Symbols like Δ and Γ are added everywhere to the “normal” symbols like A and B. There are one- and two-sided calculi. There are three different symbols for implication (⇒, ⊢ and the inference line) and three different symbols for conjunction (∧, the space above/under an inference line and the comma on the left of ⊢). And boolean and formula types are mixed with no explanation. In order to make sense of that, I came up with the following:
- Γ and Δ conjuncted and disjuncted sets of formulae, respectively, but since they are never actually split up, one can just view them as single formulae like A or B with no special meaning at all.
- Boolean objects and formulae are different data types with different corresponding operators, but are implicitly converted and interpreted depending on the context. While I understand that implicit conversion can be convenient like in C++, I find it very confusing when it is already used while explaining a new topic. When the target audience or discussion participants are not familiar enough with the topic, one should be very clear about what they are talking about, therefore I will try to explain how I understand this: Quoting (boxing) is always done implicitly. I will write “a”, which is similar to writing a
'in LISP. Evaluating (unboxing) is done either implicitly or explicitly by the unary use of ⊢, e.g. (⊢“a”)⇔a which is similar to writingevalin LISP or⍎in APL. The operators ¬, ∨, ∧, ⇒, ⇔ and the inference line operate on boolean values while the binary ⊢ connects two formulae with an implication and evaluates the result, e.g. (“a”⊢“b”)⇔(⊢“a⇒b”)⇔(a⇒b) and ≡ connects two formulae with an equality and evaluates the result, e.g. (“a”≡“b”)⇔(⊢“a⇔b”)⇔(a⇔b). Likewise, the commas to the left and right of ⊢ connect formulae with ∧ and ∨, respectively, so that ultimately (“a”,“b” ⊢ “c”,“d”)⇔a∧b⇒c∨d.
With these rules in mind, I have no problem in reading the rules and derivations on this German Wikipedia site about sequent calculus. All of the rules seem to make sense and start to feel intuitive after I look at them for some time.
In linear logic we have four dual-bool objects and four discunction and conjunction operators and the formula-operators change so that (“a”,“b”⊢“c”,“d”)=((a⊗b)⊸(c⅋d)) and (“a”≡“b”)=(a=b) (Note that I now always use = instead of ⇔ because we are no longer dealing with strictly boolean objects). The fact that ⊸ and therefore ⊢ now return objects of the dual-bool type, the behaviour of the inference line is also affected. Because of how this section about game semantics talks about validity at wins and loses, I guess it works like the following: First, the inputs are converted to boolean by converting 1 to ⊤ and 0 to ⊥ and then the normal boolean implication (⇒) is applied.
I've been having a hard time trying to obtain an intuitive understanding of all of this, since things like ⅋, ? and ! were discounted as simply “hard to understand” in various semantics and papers always started to become too complicated for me before answering important questions (in my view). I began watching the YouTube-lectures by Frank Pfenning but confusingly he uses a different subset of LL (or maybe just a different notation, I don't remember) and the popular resource semantic sometimes even appeared contradictory to me, so soon I couldn't follow up.
Then I tried to focus just on the basics and develop my own understanding of this topic, which was easier said than done because apparently no one even bothers to write truth tables, so I had to deduce the truth tables by myself which was also easier said than done because the necessary rules were scattered around.
Here's what I came up with:
- The negation is the only operation where authors were gracious enough to write down their definition directly:
| A | $(⋅)^⊥$ |
|---|---|
| 0 | ⊤ |
| ⊥ | 1 |
| 1 | ⊥ |
| ⊤ | 0 |
- The aforementioned article about game semantics helped me a lot; with its help I developed this:
| A | B | & | ⊕ | ⊗ | ⅋ |
|---|---|---|---|---|---|
| ⊥ | ⊥ | ⊥ | ⊥ | ⊥ | ⊥ |
| ⊥ | 1 | ⊥ | 1 | ⊥ | 1 |
| 1 | 1 | 1 | 1 | 1 | 1 |
| ⊥ | 0 | 0 | 0 | ||
| 1 | 0 | 0 | 1 | 0 | 0 |
| 0 | 0 | 0 | 0 | 0 | 0 |
| ⊥ | ⊤ | ⊥ | ⊤ | ⊤ | ⊤ |
| 1 | ⊤ | ⊤ | ⊤ | ||
| 0 | ⊤ | 0 | ⊤ | 0 | ⊤ |
| ⊤ | ⊤ | ⊤ | ⊤ | ⊤ | ⊤ |
Although it was not explicitly stated, I assumed that every player tries to win. However, there were unfilled gaps left in the table: These are the cases where one player has to choose between two different types of winning or losing a game. It was not explained which one was the preferred way.
- Then I read about the ! and how it can be represented as an infinite series. Since it starts with 1&, the opponent would not choose the 1 when the input is 0 or ⊥, because those are their wins, so these should stay unchanged. When the input is 1, the opponent can only choose between 1's and thus, it stays unchanged as well. When the input is ⊤, the opponent has to choose between two different types of losing. If they preferred to choose ⊤, then ! would be the identity function and therefore be quite useless. So the opponent's preferred way of losing must be 1. Because of $(!A)^⊥=?A^⊥$, the ? must work the other way round so that:
| A | ! | ? |
|---|---|---|
| 0 | 0 | ⊥ |
| ⊥ | ⊥ | ⊥ |
| 1 | 1 | 1 |
| ⊤ | 1 | ⊤ |
With this knowledge and $(A\&B)^⊥=A^⊥⊕B^⊥$, I filled the gaps in the previous table:
| A | B | & | ⊕ | ⊗ | ⅋ |
|---|---|---|---|---|---|
| ⊥ | ⊥ | ⊥ | ⊥ | ⊥ | ⊥ |
| ⊥ | 1 | ⊥ | 1 | ⊥ | 1 |
| 1 | 1 | 1 | 1 | 1 | 1 |
| ⊥ | 0 | 0 | ⊥ | 0 | 0 |
| 1 | 0 | 0 | 1 | 0 | 0 |
| 0 | 0 | 0 | 0 | 0 | 0 |
| ⊥ | ⊤ | ⊥ | ⊤ | ⊤ | ⊤ |
| 1 | ⊤ | 1 | ⊤ | ⊤ | ⊤ |
| 0 | ⊤ | 0 | ⊤ | 0 | ⊤ |
| ⊤ | ⊤ | ⊤ | ⊤ | ⊤ | ⊤ |
I then realised that if it is “always one's turn”, that means just a situation that is sometimes priorized. So you can view at it like this:
0 ⊥ 1 ⊤
<---|---------|---------|---------|--->
strong weak weak strong
falsehood falsehood truth truth
With this description, & becomes something like a min function, returning the falsest value and ⊕ becomes something like a max function, returning the truest value. ⊗ and ⅋ both return the strongest value, where in a draw, ⊗ prefers falsehood and ⅋ prefers truth. Suddenly they are easy to understand :)
! and ? (for which I have already written the truth tables), seem to act like a cap in truth and falsehood, respectively (keyword: saturation).
Because of $A⊸B=A^⊥⅋B$ the truth table for ⊸ can be derived as follows:
| A | B | ⊸ |
|---|---|---|
| 0 | 0 | ⊤ |
| ⊥ | 0 | 0 |
| 0 | ⊥ | ⊤ |
| ⊥ | ⊥ | 1 |
| 1 | 0 | 0 |
| 0 | 1 | ⊤ |
| 1 | ⊥ | ⊥ |
| ⊥ | 1 | 1 |
| 1 | 1 | 1 |
| ⊤ | 0 | 0 |
| 0 | ⊤ | ⊤ |
| ⊤ | ⊥ | 0 |
| ⊥ | ⊤ | ⊤ |
| ⊤ | 1 | 0 |
| 1 | ⊤ | ⊤ |
| ⊤ | ⊤ | ⊤ |
In classical logic, when you write true and false as 1 and 0, the implication ⇒ can be thought of as ≤, because it states that the level of truth did not decrease in the conclusion. This also applies to ⊸. The only question left is: Which level of truth/falsehood will be returned? The answer is: If at least one of the arguments is strong, the return value will be strong, otherwise weak. This feels more intuitive if we draw the truth graph with different distances like this:
0 ⊥ 1 ⊤
<---|-----------------------------|-----|-----------------------------|--->
strong weak weak strong
falsehood falsehood truth truth
If we stay on a strong level, i.e. 0⊸0 or ⊤⊸⊤, that is a strong true statement. If play in the weak level, we get ⊥ or 1. However, if we drop from ⊤ to 1 or lower, we will be punished with a strong 0 because we concluded a consequent that is so much falser than our antecedent. In contrast, if the truth increases from 0 all the way to ⊥ or even higher, that is rewarded with a strong ⊤.
With all of this in mind, all statements on this image started to make sense to me. When I just looked at them for a while and thought about the possibilities, it was eventually clear why they must be true and I was very happy about that.
The corresponding operators for the commas next to the ⊢ are the multiplicative ones (⊗ and ⅋), so while they are conjunction and disjunction, they also follow the rule that higher priority outdoes lower priority. That is the reason why you can't just add a random statement to the right of ⊢: Because the existing statements may be of weak truth and you might be adding a 0, making the whole proposition false. Similarly, you can't just remove one of multiple true statements there, because you might remove the only strong ⊤ which holds up against a 0. And if the left side of ⊢ is true you can't just add more random true statements, because you might be lifting the value of the left hand side from 1 to ⊤ and hence make the whole proposition false. This also explains why ! and ? allow for controlled weakening and contraction: They clamp their input up and down towards weakness, so that they can no longer outplay the others in the comma seperated lists.
When I realised this, I thought I finally found the essence of linear logic, and that this must be the way how this resource limitation works and since I have my own semantic now, I can forget about the resource semantic and everything will be fine. But I was wrong, because the resource semantics claim that you can have 1\$⊸candy but not 1\$⊸candy⊗candy. But, when you look at my truth table: Every time you input the same value twice into either &, ⊕, ⊗ or ⅋, you get back your input value every time, which means that candy and candy⊗candy must denote the same object which is either 0, ⊥, 1, or ⊤. I guess the resource semantic tries to say (in an irritating way), that you just cannot derive 1\$⊸candy⊗candy from the limited given axioms, although it is still true. In classical logic, you can just assume every rule that can be deduced from the truth tables of ¬, ∨ and ∧. Of course, you can debate about which of them you want choose as axioms, and if you choose too few, you might not be able to deduce every true statement from them. But usually I don't have to care much about that. I hoped that would be the same in LL. However, the essence of lineare logic seems to be to deliberately restrict the axioms even further so that you cannot deduce every true statement (like 1\$⊸candy⊗candy) anymore. And herein lies the problem: I have no idea why exactly these axioms (deduction rules) in the image are chosen, what the exact concequences are and what all of that has to do with the duality of the boolean values and the operators (Why not simply restrict axioms of classical logic instead?). And I don't feel like I'm able to figure that out all by myself any time soon.
To sum it up, here are my questions:
- Are my truth tables correct, and if not, what are the errors?
- Are all of my assumptions correct, and if not, why?
- And most important: Can someone please try to explain to me the exact reasoning behind and consequences of the choice of axioms in LL, so that I can acccomplish an intuitive understanding of which true statements can be derived and which can't? Because I feel like that's the missing part of my understanding of LL.
