- Could someone explain in simple words how linear logic connective
⊗is different from logical AND and
⊕from OR? is it that they have polarity? so it would be
⊗is equivalent of 'AND POSITIVE' and
⊕'OR POSITIVE' and
&would be 'AND NEGATIVE'?
⅋is different and similar to
⊕? they are operands that have additional property polarity so would
⊕⊥would be equivalent of our
-(minus) in a sense that opposite of
- How should I understand
(! and ?)exponentials? do they have equivalents in normal logic or maths?
- Am I reading this correctly?
A ⊸ B := A⊥
⅋ B. A and B connective is equal to Not A with B. What does this connective mean?
It's an old question but I will still try to give an answer focusing on intuition. There're a lot of intuitive interpretations of Linear Logic.
We can see Linear Logic as a Logic dealing with limited resources but also as dealing with static and non-static truths or even actions/processes : it rejects the duplication/erasure of truth/resources (contraction and weakening in Sequent Calculus). That is, we consider that :
Ais not a consequence of
(A and A)anymore because
Ais not used in the process
(A and A)is not a consequence of
Aanymore because we need two
When we want to show that a formula is a consequence of a set of formulas, every hypothesis should be used once and is consumed after each use. This process is sometimes compared to chemical reactions.
Two conjunctions and disjunctions
In Logic we can formulate the conjunction and disjunction rules in two equivalents way. For instance, for conjunction :
- Additive conjunction : from ⊢Γ,A and ⊢Γ,B we can deduce ⊢Γ,A∧B
- Multiplicative conjunction : from ⊢Γ,A and ⊢Δ,B we can deduce ⊢Γ,Δ,A∧B
where Γ and Δ are two different "contexts" containing formulas. They are equivalent if we consider arbitrary duplication and erasure of formulas but they are no longer equivalent when we forbid them : it's a refinement of the usual logic.
The forbidding of structural rules give birth to two different conjunctions and disjunctions. You can find the definitions of the rules in Wikipedia.
- Additive conjunction & (with) : when reading the rules in the reverse order, if we have a proof of ⊢Γ,A&B then we have a proof of ⊢Γ,A and ⊢Γ,B but not both since Γ is entirely consumed in the process of producing either A or B. It can be seen as an active choice : choose to have A or B but not simultaneously.
- Multiplicative conjunction ⊗ (tensor) : the resources are shared, we can produce both A and B simultaneously.
- Additive disjunction ⊕ (plus) : it can be seen as a passive choice, we can take either the path of proving A or B but we don't known which one holds (it may lead to a lack or extra resources).
- Multiplication disjunction ⅋ (par) : more difficult to give an intuitive interpretation but some see a parallelization of processes
The negation is called dual (⊥ or ~) and is no longer seen as the usual negation. It's used to converts hypothesis to conclusion :
Γ⊢A means that we can consume the formulas of
Γ to produce
A but since the duality is involutive
(~~A = A),
Γ⊢A is the same as
(~Γ) is the dual of all the formulas of
We can observe that it divides the rules by two (as we can see in the Wikipedia page). Girard sometimes uses the expression "hegelian negation" to refer to linear duality. Duality define a symmetry between hypothesis and conclusion. We can also see
~A as a consumer of
The relation between the operators are given by duality :
- ~(A⊗B) = ~A ⅋ ~B
- ~(A⊕B) = ~A & ~B
It's similar to the duality between ∧ and ∨ but with two conjunctions and disjunctions.
A ⊸ B is actually a shortcut for
~A ⅋ B. More generally,
~(A⊗B) is also a shortcut for
~A ⅋ ~B and are not only "logically equivalent" but equal.
A ⊸ B means : by consuming
A we can produce
B. In the alternative syntax,
~A ⅋ B can be read "consumes A and produces B in parallel".
! (bang/of course) and
? (why not) re-introduce the potential infinity we lost by forbidding duplication/erasure.
!A can be read "as many
A as we want".
They don't have equivalents in the regular logic because they're hidden : the usual implication
A→B is actually refined to
!A ⊸ B in linear logic. In the usual logic (classical or intuitionistic) truths are static so when we know
A we can use
A→B as many times as we want to prove
We can actually redefine classical and intuitionnistic logic from linear logic with the exponentials.
? is just the dual of
! that is : potential infinity occuring in the hypothesis. If we have
!A⊢A it becomes
⊢~(?A),A. It's the symmetry between hypothesis and conclusion provided by duality.