I'm trying to understand linear logic to understand linear type systems better. However, when I read the rules, I fail to get an intuition behind it as I've done in modal logic - $\Box A$ means $A$ is required as in Kripke frames $A$ is required for every reachable world [$\Diamond A$ is $A$ is possible mutatis mutandis]. But I cannot find any intuitive explanation for duality and which of conjunction / disjunction pairs (if any) corresponds to $\land$ and $\lor$.
What is the intuition behind linear logic?
lo.logic;type theory;linear logic
I'm not sure this question is ideal for CSTheory, but given that it's already gathering upvotes, here is an  answer somebody might have given had the question  been posted on cs.stackexchange.In order to understand linear logic's notion of duality $(\cdot)^{\bot}$,which forces conjunction and disjunction apart much further than we are used to in conventional logic, I recommendnot   to think of linear logic in terms of resources (although this is  an important reading). Instead  think of linear logic formulae $A$  as processes that communicate  at a port / name / channel. This interpretation has been fleshed out first in (1) to the best of my knowledge, but it's already alluded to in Girard's original work. As a picture:                    (I'm not sure how properly to center images here.)Linear conjunction $A \otimes B$ is interpreted as running processes $A$  and $B$ in parallel.  The process $A \otimes B$  communicates pairs $(a, b)$ at its port, where $a$ comes from  $A$ and $b$ is $B$'s communication.                  Dualisation $(.)^{\bot}$ (which is linear logic's  negation) switches input and output. Hence the dual of $A \otimes B$  is$$  (A \otimes B)^{\bot} \quad = \quad A^{\bot}  B^{\bot}  $$In this reading $A^{\bot}   B^{\bot}$ is the process that communicates with $A \otimes B$.Linear logic's equivalent of disjunction can  be given a similar process-theoretic reading. The formula$$  A\ \&\ B  $$should also be seen as  two processes $A$ and $B$ in parallel, but rather than actively sending messages, they wait for  the environment to decide which to run. So $A \& B$ sits there,  waiting on its channel for a bit of information which decides if $A  \& B$ should run as $A$ or as $B$. This is a 'parallel' version of  the $if/then/else$ in sequential programmaning languages. The dual  $(A \& B)^{\bot}$ of $A \& B$ is$$  (A \& B)^{\bot} \quad = \quad A^{\bot} \oplus B^{\bot}  $$can be seen as a process sending 1 bit of information to $A \&  B$, namely: continue as $A$ or continue as $B$. This is similar to in  $if\ true\ then\ P\ else\ Q$ evaluating to $P$ while  $if\ false\ then\ P\ else\ Q$ evaluating to $Q$, except thatthe choice between $A$ and $B$ is now made by the environment.  The !-operator also has a process-theoretic interpretation: if $A$  is read as a process, then $!A$ can be read as running infinitely  many processes $A$ in parallel.In this reading the axioms $A \vdash A$ of linear logic become simple 'wires' that forward messages from processes $A^{\bot}$ to processes $A$. This interpretation of axioms is already in Girard's proof nets (3).This process-theoretic interpretation  has been influential and  given rise to a lot of follow-up work like e.g. (2) for session types. Nevertheless, there are someedge cases that make it a bit awkward, and to the best of my knowledge  it hasn't been made to work perfectly for full linear logic even in 2017. 1. S. Abramsky, Computational Interpretations of Linear Logic.2. P. Wadler, Propositions as sessions.3. Wikipedia, Proof net.