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.

Filter by
Sorted by
Tagged with
1
vote
0answers
11 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 ...
0
votes
0answers
41 views

Distributive property of tensor ($\otimes$) over par (⅋) in linear logic

In the setting of linear logic, does $\otimes$ distribute over $⅋$? That is, is it possible to show that $$ A \otimes (B ⅋ C) \stackrel?\equiv (A \otimes B) ⅋ (A \otimes C) $$ holds? If not, what ...
1
vote
1answer
74 views

Is $A \& B ⊸ A$ derivable?

Intuitively, the sentence $A \& B ⊸ 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 way to ...
2
votes
0answers
104 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$...
3
votes
2answers
122 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 ...
4
votes
1answer
87 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 ...
3
votes
1answer
72 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 \...
3
votes
2answers
136 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 ...
3
votes
0answers
56 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 ...
9
votes
1answer
274 views

Why is it called linear logic?

Why is it called "Linear" Logic? What's linear about it?
4
votes
0answers
70 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.
3
votes
1answer
57 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 ...
3
votes
1answer
77 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: ...
12
votes
2answers
755 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 ...
7
votes
2answers
361 views

What is the intutition 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 $a$...
7
votes
0answers
398 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 (...
4
votes
2answers
274 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?
9
votes
2answers
982 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 ...
4
votes
2answers
112 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.
10
votes
1answer
347 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 ...
7
votes
3answers
429 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
3answers
307 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 \...
5
votes
0answers
52 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 ...
4
votes
1answer
193 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 ...
6
votes
1answer
181 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$, ...
22
votes
5answers
4k 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$ ...