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
0
votes
0answers
18 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 ...
2
votes
1answer
64 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 ...
4
votes
1answer
45 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
2answers
123 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 ...
1
vote
0answers
18 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 ...
3
votes
1answer
120 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) $$ ...
3
votes
2answers
123 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 ...
2
votes
0answers
141 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
160 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
105 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
79 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
173 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
62 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
493 views

Why is it called linear logic?

Why is it called "Linear" Logic? What's linear about it?
4
votes
0answers
86 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
73 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
88 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
955 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
421 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$...
8
votes
0answers
473 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
412 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
1k 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
139 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
415 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
506 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
356 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
59 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
202 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
208 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$, ...
23
votes
6answers
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$ ...