# Questions tagged [linear-logic]

The tag has no usage guidance.

24 questions
Filter by
Sorted by
Tagged with
212 views

### Distributivity of ! over?

Has anyone studied a variant of linear logic, or of its semantic counterpart (exponential modalities on linearly distributive categories / $\ast$-autonomous categories / polycategories) for which ...
132 views

### Internal logic in topos theory, monoidal categories, and quantum mechanics

To obtain the internal logic of a topos (roughly speaking), we associate a type of free variable with an object, and a statement about such a variable with a subobject of that object. Intuitively, the ...
166 views

### What is the sequent calculus for differential linear logic? [closed]

I have searched, but only managed to turn up the presentation in interaction nets. I'd be equally interested in a categorical model of DiLL.
111 views

### Lambek calculus, linear logic, and linear algebra

In his 1958 paper, The Mathematics of Sentence Structure, Joachim Lambek introduced the Lambek calculus. In modern terms, it could be understood as a syntax for biclosed monoidal categories, and he ...
357 views

### Proof of ¬(¬1 ⊗ ¬1) in tensorial logic

I believe I once had a proof of this proposition, but it's been lost to the mists of time and old hard drives, so who knows if it was correct, and try as I might I can't seem to reproduce it. Is it ...
115 views

Has anyone studied a version of linear logic in which the storage modality $!$ preserves the positive connectives and quantifiers $\otimes,\oplus,\exists$? That is, such that we have $!(A\otimes B) = ... 1answer 431 views ### Is Girard's LU just an embedding of classical and intuitionistic logic into linear logic? This question is about Girard's system LU, presented in his paper On the unity of logic. Girard starts by giving a "modal" sequent calculus with two zones of both hypotheses and consequents,$\Gamma;\...
338 views

As defined by Gan, a dioperad consists of sets of operations $P(n,m)$ with "$n$ inputs and $m$ outputs", which can be composed by joining one output of one operation to one input of another, giving ...
131 views

### Differential categories vs McBride's notion of derivative

Has anyone done an analysis to see if Blute, Cockett, and Seely's differential categories suffice to provide a notion of 1-hole context in the symmetric monoidal setting?
186 views

### Can a relationship be constructed between the Coherence space and Phase space semantics of linear logic?

I'm not very familiar with linear logic, so please bear with me, i.e., please "read between the lines" to my underlying question if I don't formulate it rigorously correctly. To help model some of my ...
391 views

### Embedding of classical into intuitionistic linear logic

Following on from this recent question, there is another construction that is well-known, but I don’t know a good primary source for: the Kolmogorov-style double-negation embedding of classical into ...
311 views

### Conservativity of multiplicative linear logic over intuitionistic multiplicative linear logic

It is well known that multiplicative linear logic (MLL) is conservative over intuitionistic multiplicative linear logic (IMLL). In other words, if an IMLL formula is provable in MLL then it is already ...
84 views

225 views

### Is it possible to implement η-reduction in interaction nets?

There are several ways to encode λ-terms in interaction nets; for instance, using the original optimal algorithm by Lamping, or compiling λ-calculus into interaction combinators. However, all the ...
128 views

369 views

### Looking for papers and articles on the Tarskian Möglichkeit

Some background: Łukasiewicz many-valued logics were intended as modal logics, and Łukasiewicz gave an extensional definition of the modal operator: $\Diamond A =_{def} \neg A \to A$ (which he ...
Multiplicative intuitionistic linear logic (MILL) has only multiplicative conjunction $\otimes$ and linear implication $\multimap$ as connectives. It has models in symmetric monoidal closed ...