5
$\begingroup$

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:

  1. Γ 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.
  2. 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 writing eval in 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:

  1. The negation is the only operation where authors were gracious enough to write down their definition directly:
A $(⋅)^⊥$
0
1
1
0
  1. 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.

  1. 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 :)

  1. ! and ? (for which I have already written the truth tables), seem to act like a cap in truth and falsehood, respectively (keyword: saturation).

  2. 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.
$\endgroup$
2
  • $\begingroup$ About your last question: you say you are "very interested in proof search". Proof search must be done in some proof system. Which proof systems are you familiar with? Sequent calculus is one such proof system, it is certainly different than others, but it can be related to them. If you tell us which system you already know, maybe someone can point you to somewhere where this relationship is explained. After you understand sequent calculus, linear logic is easier to understand. $\endgroup$ Feb 22 at 13:49
  • $\begingroup$ Also, what "intuitive understanding of which true statements can be derived and which can't" do you expect to obtain? For example, do you have such an intuitive understanding for classical logic? Explaining it maybe can help people understand what you are looking for with respect to linear logic. $\endgroup$ Feb 22 at 13:51

1 Answer 1

10
$\begingroup$

The following answers your first two questions.

It seems to me that you're working under the assumption that propositional linear logic is a 4-valued logic, in the same sense that propositional classical logic is a 2-valued logic. This is wrong. You will never understand linear logic if you think in terms of truth values. The same holds for intuitionistic logic, which linear logic refines.

(In fact, linear logic does admit a truth semantics, but I'm afraid you'd find it even more "irritating" than the one you call "resource semantics"--try and Google "linear logic phase semantics". That's why "no one even bothers to write truth tables").

Intuitionistic logic and linear logic are best understood in terms of proofs rather than provability, that is, you don't just look at what you can prove but at how you prove it. This is how, for example, intuitionistic logic sees the difference between $A\lor B$ (one of $A$ or $B$ holds) and $\lnot\lnot(A\lor B)$ (it is impossible that none among $A$ and $B$ holds): the first is proved by explicitly showing one of $A$ or $B$; the second, typically, by assuming $\lnot(A\lor B)$ and deriving a contradiction, so you don't know which one actually holds. The two formulas have the same truth value, but their proofs have very different logical content and, once you consider the right set of logical rules, the formulas are no longer provable one from the other (as they are in classical logic).

Intuitively, linear logic refines intuitionistic logic by looking at how many times you used a certain assumption to prove something. If you think in terms of truth, this is nonsensical: mathematical truth is "inexhaustible", it is untarnished by use. In spite of having been used countless times in countless proofs through the millennia, the Pythagorean theorem is just as true today as it was when it was first discovered. But in terms of the structure of proofs, allowing arbitrary reuse does make a difference, which is reflected, for example, in the existence of two different disjunctions $A\oplus B$ and $A\mathrel{\text{⅋}} B$, which behave (kind of) like the two different meanings of $\lor$ explained above.

Linear logic has deep connections with programming languages, where linearity turns out to be related, very approximately, to how many times a program accesses memory, something that makes a lot of sense, but not from the viewpoint of truth. It also has applications to proof search, which you find described in the Stanford Encyclopedia article you linked to. Again, these applications concern the way you prove things, in particular how you may eliminate some of the non-determinism in proof search.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.