# 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
Filter by
Sorted by
Tagged with
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 ...
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 ...
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 &...
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 ...
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$. ...
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 ...
107 views

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 ...
1 vote
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 ...
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)$$ ...
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 ...
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$...
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 ...
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 ...
95 views

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 (...
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?
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 ...
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.
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 ...
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 ...
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 \...
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 ...
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 ...
### 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$, ...
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$ ...