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
2 votes
0 answers
39 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 ...
user avatar
  • 1,938
6 votes
1 answer
164 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, ...
user avatar
  • 1,938
5 votes
1 answer
85 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 ...
user avatar
  • 1,938
3 votes
1 answer
52 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 ...
user avatar
  • 315
6 votes
0 answers
161 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 \...
user avatar
  • 1,938
0 votes
0 answers
23 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 ...
user avatar
  • 205
2 votes
1 answer
66 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 ...
user avatar
3 votes
0 answers
65 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 ...
user avatar
0 votes
0 answers
29 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 ...
user avatar
  • 221
4 votes
1 answer
78 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 ...
user avatar
  • 77
4 votes
1 answer
123 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(...
user avatar
2 votes
2 answers
149 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 ...
user avatar
  • 156
1 vote
0 answers
25 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 ...
user avatar
  • 163
5 votes
1 answer
184 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) $$ ...
user avatar
3 votes
2 answers
151 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 ...
user avatar
  • 198
2 votes
0 answers
315 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$...
user avatar
3 votes
2 answers
348 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 ...
user avatar
4 votes
1 answer
134 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 ...
user avatar
  • 699
3 votes
1 answer
85 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 \...
user avatar
  • 67
3 votes
2 answers
237 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 ...
user avatar
  • 1,373
4 votes
0 answers
80 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 ...
user avatar
  • 1,373
11 votes
1 answer
738 views

Why is it called linear logic?

Why is it called "Linear" Logic? What's linear about it?
user avatar
  • 213
5 votes
0 answers
110 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.
user avatar
3 votes
1 answer
85 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 ...
user avatar
3 votes
1 answer
99 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: ...
user avatar
  • 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 ...
user avatar
  • 441
12 votes
2 answers
545 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 $...
user avatar
10 votes
0 answers
548 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 (...
user avatar
4 votes
2 answers
706 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?
user avatar
  • 1,373
10 votes
2 answers
2k 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 ...
user avatar
4 votes
2 answers
173 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.
user avatar
  • 1,373
10 votes
1 answer
510 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 ...
user avatar
  • 203
7 votes
3 answers
605 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 ...
user avatar
6 votes
3 answers
455 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 \...
user avatar
5 votes
0 answers
62 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 ...
user avatar
4 votes
1 answer
228 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 ...
user avatar
  • 1,125
6 votes
1 answer
259 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$, ...
user avatar
  • 8,915
28 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$ ...
user avatar
  • 383