Questions tagged [linear-logic]
Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter. Ideas from linear logic have been influential in fields such as programming languages, game semantics, and quantum physics, as well as linguistics, particularly because of its emphasis on resource-boundedness, duality, and interaction.
46
questions
2
votes
2
answers
444
views
Linear logic proof of $P⊸(Q⊸R)≡(P⊗Q)⊸R$?
I’ve been trying to use https://click-and-collect.linear-logic.org for a while, and have been thinking about exportation/importation for Linear Logic. Intuitively, I thought P⊸(Q⊸R)≡(P⊗Q)⊸R was valid ...
- 933
3
votes
1
answer
61
views
Distributivity of ⊗ over & in linear logic?
In linear logic, we have that multiplicative conjunction distributes over additive conjunction:
$$(A\ \&\ B) \otimes C ⊸ (A \otimes C)\ \&\ (B \otimes C).$$
But we do not have the other ...
- 33
3
votes
1
answer
57
views
Is there a "standard" normal form for formulas in linear logic?
For propositional logic, for every formula, there is an equivalent formula in the CNF and DNF. These normal forms have the advantage of being representable in a "tabular" form rather than a &...
- 132
4
votes
1
answer
119
views
Linear logic as Fitch-style natural deduction?
I've recently been looking into linear logic, and it seems every source I can find on it uses the sequent calculus proof system. However, I personally find the sequent calculus to have numerous ...
- 442
0
votes
0
answers
60
views
The semantics of until operator in linear temporal logic
According to the definition of until operator from Wiki:
$w \models \varphi~\text{U}~\psi$ if there exists $i \geq 0$ such that $w^i \models \psi$ and for all $0 \leq k < i, w^k \models \varphi$.
...
- 377
0
votes
1
answer
69
views
Linear Logic Question About Exponentials
In Linear Logic (L.L.), exponentials {!,?} are used to allow the rules of Weakening and Contraction for formulas under their scope. It is a theorem of Linear Logic that
!(P⊗Q)⊸!(P&Q) where ‘⊗’ is ...
- 933
0
votes
0
answers
107
views
Sequent calculus as multilinear/tensor algebra?
Settings
I have been studying sequent calculus for several months and found that there should be a rule that is seemingly typical, even too trivial, but/hence no one officially mentions:
$$
\dfrac{
a ...
- 1
0
votes
0
answers
31
views
Abbreviations for variants of mLL?
1. Context
There are various variants of multiplicative linear logic (mLL). I am wondering how those various relatives of mLL are conventionally abbreviated.
2. Question
What are common abbreviations ...
- 2,858
2
votes
0
answers
45
views
Linearly distributive categories: Principles of excluded middle and contradiction
1. Context
Let $(\mathscr{C}, \otimes, \top, \oplus, \bot, \delta ^l, \delta^r)$ be a linearly distributive category.
Let $(S,S', \alpha, \beta, \alpha‘, \beta‘)$ be a negation on $\mathscr{C}$. This ...
- 2,858
6
votes
1
answer
260
views
Linear logic and linearly distributive categories
1. Context
On page two of the introduction to their paper Weakly distributive categories on linearly distributive categories Cockett and Seely write:
It turns out that these weak distributivity maps, ...
- 2,858
5
votes
2
answers
268
views
Why is multiplicative disjunction called "par" in linear logic?
In linear logic multiplicative disjunction is often called par.
This terminology goes back at least to Girard's seminal text Linear logic. I vaguely remember that I read that "par" is an ...
- 2,858
3
votes
1
answer
85
views
Is $A ⅋ (B \otimes C) \vdash (A⅋B) \otimes C$ provable in MLL?
Consider the multiplicative fragment of linear logic (MLL) which only consists of the multiplicative connectives tensor and par together with the inference rules axiom, cut, $\otimes$ and ⅋. I was ...
- 1,029
6
votes
1
answer
222
views
Graphical calculus for star-autonomous categories?
1. Definiton
Let $(C, \otimes, I, a, l,r)$ be a (not necessarily symmetric) monoidal category.
A (planar) star-autonomous structure on the monoidal category $C$ consists of an adjoint equivalence $D \...
- 2,858
0
votes
0
answers
45
views
What is the interpretation for $A^\bot$ in Linear logic?
I was reading the wikipedia page for linear logic https://en.wikipedia.org/wiki/Linear_logic
At some point it shows that a proposition may be raised to bottom as in $A^\bot$, what is the ...
- 225
2
votes
1
answer
91
views
What is the resource interpretation of $A \to B$ in linear logic?
Linear logic seems to have two forms of implication.
$$A \multimap B$$
With resource interpretation of "consuming A yields B".
And the usual
$$A \rightarrow B$$
What is the resource ...
- 53
3
votes
0
answers
71
views
Is there a linear logic/category that deals with real quantities of resources?
Linear logic models consumption of discrete resources.
Q: Is there an extension of linear logic that models the consumption of numeric resources (e.g., amount of a chemical substance).
Q: If so, does ...
- 53
0
votes
0
answers
30
views
What flavours of Linear Logic are algebraizable?
I am a theoretical linguistics student and I have been working in the last few years on an improved model of natural language semantics, but I am missing a final mathematical insight in order to wrap ...
- 221
4
votes
1
answer
101
views
English Sentences to Linear Logic
I need to convert the following sentences to Linear Logic formulas-:
1) Bob can spend $1 to purchase a bottle of water or a bag of chips (Bob's
choice). (D means Bob has a dollar; W means Bob has a ...
- 77
4
votes
1
answer
178
views
Substructural Logic: Understanding the roles of Weakening and Contraction
I am trying to understand the "structural" rules of logic, and how relaxing/adding certain these rules gives rise to different types of logic (linear, affine, etc.)
The rules are
Exchange: $$\left(...
2
votes
2
answers
163
views
Resource Metalogic: Proving that a theorem can (not) be deduced from given axioms in a certain number of steps
One of the reasons automated theorem proving systems haven't caught up with humans yet might be that they have no intuition about resource exploration vs exploitation and other evolved heuristics, due ...
- 138
1
vote
0
answers
27
views
What are the differences between a linear logic based planner and a first order logic based planner
Linear logic based planners and first order logic based planners must have different strengths and weaknesses. I would appreciate help in understanding what these strengths and weaknesses are and ...
- 183
5
votes
1
answer
270
views
Distributive property of tensor ($\otimes$) over par (⅋) in linear logic
In the setting of linear logic, does the tensor $\otimes$ distribute over the par $⅋$?
That is, is it possible to show that
$$
A \otimes (B ⅋ C) \stackrel?\equiv
(A \otimes B) ⅋ (A \otimes C)
$$
...
- 163
3
votes
2
answers
166
views
Is $A \& B \multimap A$ derivable?
Intuitively, the sentence $A \& B \multimap A$ seems to mean "Using a choice between $A$ and $B$, get an $A$." This feels like it should be derivable for any $A$ and $B$, but I haven't found any ...
- 218
2
votes
0
answers
324
views
For every formula of linear logic, is there an equivalent formula in intuitionistic linear logic?
Consider the sequent calculus presentations of propositional linear logic (LL) and propositional intuitionistic linear logic (ILL). Clearly, there are formulas in LL that are not in ILL, such as $\bot$...
- 16.3k
3
votes
2
answers
387
views
About the internal hom in a symmetric monoidal closed category
Let $\mathcal{C}$ be a symmetric monoidal closed category. My question is the following:
Given three objects $X$, $Y$ and $Z$, and a morphism $f \colon Y \to Z$ in $\mathcal{C}$, does it ...
- 16.3k
4
votes
1
answer
151
views
How can we interpret that $A, B \vdash A, B$ is unprovable with resource interpretation in Linear Logic?
In Linear logic (LL), it is unprovable but when considering the resource interpretation it seems to me that from the resources $A, B$ we can produce the resources $A, B$.
By $A, B \vdash A, B$ I mean ...
- 739
3
votes
1
answer
95
views
Proving Negation Identity in Intuitionistic Linear Logic
In a Gentzen system (i.e. sequent calculus) for Intuitionistic Linear Logic (from now, ILL), given the usual rules for ILL ($\wedge L, \wedge R, \circ L, etc.$), I want to prove that the Identity $A \...
- 67
3
votes
2
answers
283
views
Is currying valid in Linear logic and Relevance logic?
In Classical and Intuitionistic logic we have what I will call the "currying equivalence":
$P \rightarrow (Q \rightarrow P) \equiv (P \land Q) \rightarrow P$
But linear and relevance logics do not ...
- 1,443
4
votes
0
answers
81
views
Transforming intuitionistic propositional validities into validities of linear logic
A tableaux method for linear logic is briefly discussed in
https://www.academia.edu/6591354/TABLEAU_METHODS_FOR_SUBSTRUCTURAL_LOGICS?auto=download
D'Agostino writes (p.418-9):
''It is ...
- 1,443
13
votes
1
answer
914
views
5
votes
0
answers
129
views
Resource request: linear logic
Is there any correct book/textbook/pdf to understand what is linear logic ? I do research in (standard) logic/model theory, so I'm totally ok with a text which assumes mathematical maturity.
- 200
3
votes
1
answer
103
views
Can I derive $ \vdash \Gamma $ from $ \vdash \Gamma, A, A^\bot $?
The Wikipedia article on linear logic mentions the following as an initial sequent:
$$ \over \vdash A, A^\bot $$
As far as I can understand from informal descriptions of linear-logic semantics, this ...
- 133
3
votes
1
answer
110
views
Basic equivalences in linear logic
How do we obtain the equivalence $A \otimes 0 \equiv 0$ and its dual in linear logic? Are they a consequence of cut-elimination?
I found them listed as basic equivalences in the following resource: ...
- 31
14
votes
2
answers
1k
views
About Jean-Yves Girard
I am student and I'm studying linear logic. I saw a quote in a book:
"I'm not a linear logician" - Jean-Yves Girard. Tokyo, April 1996.
I searched on Google but I did not find the context of why he ...
- 451
12
votes
2
answers
703
views
What is the intuition behind the negative exponential '?' in linear logic?
The positive exponential $!$ has a very satisfying interpretation in terms of the standard resource interpretation of linear logic. Given a resource $a$, we know that $!a$ means an infinite supply of $...
- 3,145
12
votes
0
answers
645
views
Why don't the quantifiers split in linear logic?
Every presentation of linear logic I've seen seems to either omit or treat quantifiers as an after-thought. Even Girard says that there is "little to say" about them. However, if we view universal (...
- 570
4
votes
2
answers
895
views
Implication in linear logic
Linear logic abandons the structural rules of weakening and contraction.
I wanted to know whether we have $p ⊸ p$ in linear logic.
Can anyone help?
- 1,443
10
votes
2
answers
3k
views
What is the difference between intuitionistic, classical, modal and linear logic?
I am currently going through Philip Wadler's "Proposition as Types" and a passage of the introduction has struck me:
Propositions as Types is a notion with breadth. It applies to a
range of ...
- 827
4
votes
2
answers
192
views
Models of Linear Logic
I am looking for an introduction to the model theory of Linear Logic. Can you recommend any clear introductions?
I am particularly interested in those models that regard coherence spaces.
- 1,443
10
votes
1
answer
626
views
Defined negation in intuitionistic linear logic
Is it possible to define a negation in intuitionistic linear logic, the way one does in intuitionistic logic, i.e. $A^{\bot} \equiv A \multimap \mathbf{0}$ (or, as it would be written in ...
- 203
7
votes
3
answers
691
views
Linear Logic, what is it used for?
I read a lot about Linear Logic recently but I failed to find any real use to the logic.
I'd like to know how and where Linear Logic could be applied. Something like lambda calculus can be clearly ...
6
votes
3
answers
524
views
De Morgan laws of linear logic
I find it stated, in all the resources I have searched, that the following De Morgan laws$$(A\otimes B)^{\perp}\equiv A^{\perp}\wp B^{\perp}\quad\quad\quad (A\text{&}B)^{\perp}\equiv A^\perp \...
- 4,948
5
votes
0
answers
67
views
Logics for resource control over time
I'm studying proof theory and I've seen that linear logic can be used as a "way" to control resources usage, since by the propositions-as-types it is equivalent to the linear lambda calculus.
Is ...
- 151
4
votes
1
answer
255
views
Intuitionistic Linear Logic
I am currently going through some papers that use the "intuitionistic version" of Girard's Linear Logic. The problem is that I seem to find very little literature on it. There is a lot done on Linear ...
- 1,135
6
votes
1
answer
292
views
In linear logic sequent calculus, can $\Gamma \vdash \Delta$ and $\Sigma \vdash \Pi$ be combined to get $\Gamma, \Sigma \vdash \Delta, \Pi$?
Linear logic is a certain variant of sequent calculus that does not generally allow contraction and weakening. Sequent calculus does admit the cut rule: given contexts $\Gamma$, $\Sigma$, $\Delta$, ...
- 9,604
29
votes
6
answers
5k
views
What is the intuition behind the "par" operator in linear logic?
I'm $\DeclareMathOperator{\par}{\unicode{8523}}$ trying to wrap my mind around the $\par$ ("par") operator of linear logic.
The other connectives have simple resource interpretations ($A\otimes B$ ...
- 393