Skip to main content

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
1 answer
37 views

Is linear logic with the mix rule truth functional?

Linear logic is not truth functional. If one tries, in the style of classical propositional logic, to make a truth table for $A \otimes B$, $A ⅋ B$, $A \& B$, and $A \oplus B$, for $A,B \in \{0,\...
Erik T's user avatar
  • 80
2 votes
1 answer
43 views

Linear logic: Coherence space semantics for non-atomic formulas

In Jean-Yves Girard's "Between logic and quantic: a tract" (2004) the coherence space semantics of linear logic is explained. First, Girard introduces the notion of a carrier set $\mathbb{X}$...
Erik T's user avatar
  • 80
1 vote
1 answer
58 views

Linear logic with contraction

What is the proof system obtained when adding a contraction rule to linear logic or removing the weakening rule from intuitionistic logic? In other words, what goes in the missing cell of the ...
user avatar
2 votes
2 answers
501 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 ...
PW_246's user avatar
  • 1,383
4 votes
1 answer
87 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 ...
exp's user avatar
  • 43
4 votes
1 answer
93 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 &...
user1747134's user avatar
4 votes
1 answer
170 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 ...
Nico's user avatar
  • 452
0 votes
0 answers
73 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$. ...
maplgebra's user avatar
  • 377
0 votes
1 answer
112 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 ...
PW_246's user avatar
  • 1,383
0 votes
0 answers
113 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 ...
Rin's user avatar
  • 1
0 votes
0 answers
34 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 ...
Max Demirdilek's user avatar
2 votes
0 answers
54 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 ...
Max Demirdilek's user avatar
6 votes
1 answer
294 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, ...
Max Demirdilek's user avatar
5 votes
2 answers
407 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 ...
Max Demirdilek's user avatar
3 votes
1 answer
100 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 ...
Margaret's user avatar
  • 1,769
6 votes
1 answer
261 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 \...
Max Demirdilek's user avatar
0 votes
0 answers
74 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 ...
geckos's user avatar
  • 225
2 votes
1 answer
105 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 ...
idomorphism's user avatar
3 votes
0 answers
78 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 ...
idomorphism's user avatar
0 votes
0 answers
35 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 ...
eslukas's user avatar
  • 241
4 votes
1 answer
118 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 ...
hjuk12's user avatar
  • 77
4 votes
1 answer
222 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(...
bumbling-tadpole's user avatar
2 votes
2 answers
169 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 ...
2080's user avatar
  • 150
1 vote
0 answers
31 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 ...
san's user avatar
  • 193
5 votes
1 answer
316 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) $$ ...
Andrea Censi's user avatar
3 votes
2 answers
180 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 ...
Woofmao's user avatar
  • 228
2 votes
0 answers
334 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$...
Taroccoesbrocco's user avatar
3 votes
2 answers
453 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 ...
Taroccoesbrocco's user avatar
4 votes
1 answer
175 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 ...
Boris's user avatar
  • 759
3 votes
1 answer
101 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 \...
Rameau's user avatar
  • 67
3 votes
2 answers
311 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 ...
user65526's user avatar
  • 1,413
4 votes
0 answers
84 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 ...
user65526's user avatar
  • 1,413
13 votes
1 answer
1k views

Why is it called linear logic?

Why is it called "Linear" Logic? What's linear about it?
psquid's user avatar
  • 233
5 votes
0 answers
142 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.
Arthur Milchior's user avatar
3 votes
1 answer
109 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 ...
Seth Gordon's user avatar
3 votes
1 answer
125 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: ...
Andrea's 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 ...
Laura's user avatar
  • 471
13 votes
2 answers
889 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 $...
Nathan BeDell's user avatar
12 votes
0 answers
703 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 (...
user181407's user avatar
4 votes
2 answers
997 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?
user65526's user avatar
  • 1,413
10 votes
2 answers
4k 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 ...
Erwan Aaron's user avatar
4 votes
2 answers
219 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.
user65526's user avatar
  • 1,413
10 votes
1 answer
694 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 ...
wen's user avatar
  • 203
7 votes
3 answers
778 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 ...
Loïc Faure-Lacroix's user avatar
6 votes
3 answers
615 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 \...
Self-teaching worker's user avatar
5 votes
0 answers
69 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 ...
Rodrigo Ribeiro's user avatar
4 votes
1 answer
272 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 ...
essay's user avatar
  • 1,125
6 votes
1 answer
322 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$, ...
Tanner Swett's user avatar
  • 10.7k
31 votes
6 answers
6k 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$ ...
hmp's user avatar
  • 413