# Questions tagged [linear-logic]

The linear-logic tag has no usage guidance.

**4**

votes

**0**answers

46 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 ...

**6**

votes

**1**answer

318 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 ...

**6**

votes

**0**answers

95 views

### Linear logic with storage preserving positives

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) = ...

**10**

votes

**1**answer

333 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;\...

**7**

votes

**1**answer

265 views

### Dioperads vs polycategories

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 ...

**0**

votes

**1**answer

120 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?

**1**

vote

**0**answers

181 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 ...

**5**

votes

**1**answer

355 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 ...

**6**

votes

**1**answer

281 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 ...

**1**

vote

**1**answer

80 views

### Injecting premises into two implicational premises connected by a tensor (multiplicative conjunction) in linear logic

I have another question regarding linear logic: I want to get to the proof E, using the premises in (1-4). Is this at all possible?
1: $A$
2: $C$
3: $(A\multimap B)\otimes(C\multimap D)$
4: $B\...

**0**

votes

**0**answers

111 views

### Dissolution of Tensors

I have a question that might seem odd to linear logic experts (I am somewhat of a novice). I know that two items of the same type can be combined into one premise with a tensor (multiplicative ...

**6**

votes

**3**answers

392 views

### Models of intuitionistic linear logic that reflect the resource interpretation

I am interested in models of intuitionistic linear logic, that is, the logic that you get if you take classical linear logic and restrict the set of operators to $\otimes$, $1$, $\multimap$, $\times$, ...

**4**

votes

**3**answers

538 views

### Exponentials in the opposite category of finite separable algebras

Let $K$ be a field and $G=Gal(K_s/K)$ is its absolute Galois group. Then, by Galois theory, the category of finite separable algebras over $K$ (denoted by $Sep(K)$) and the category of finite ...

**1**

vote

**1**answer

159 views

### Interaction-based approximation for HP-complete λ-theory?

We are looking for a proof or counter-examples for the following hypothesis.
Two combinators $M$ and $N$ are solvable and equivalent in the HP-complete sensible $\lambda$-theory iff either
$$
\exists ...

**1**

vote

**1**answer

208 views

### Hypothesis: interaction-based model for λKβη

We are looking for a proof or counter-examples to the following
Hypothesis. In interaction calculus $\langle \varnothing\ |\ \Gamma(M, x) \cup \Gamma(N, x)\rangle \downarrow \langle \varnothing\ |\ ...

**4**

votes

**0**answers

212 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 ...

**1**

vote

**0**answers

126 views

### Turing-complete primitive interaction systems

Let us call primitive an interaction system with the signature
$\Sigma = \{(\rho, 0), (\xi, n)\}, \quad n \geq 2;$
and the only rule being of the form
$\rho \bowtie \xi[\rho, \xi(a_1, \dots , a_n), ...

**5**

votes

**2**answers

527 views

### Are exponentials in categorical models of linear logic harmful?

Categorical models for linear logic with $\otimes$, $1$, $\&$, $\top$, $\oplus$, $0$, and $\multimap$ are typically symmetric monoidal closed categories (for modeling $\otimes$, $1$, and $\...

**7**

votes

**1**answer

358 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 ...

**14**

votes

**1**answer

816 views

### How is Fredkin and Toffoli's Conservative Logic related to Linear Logic?

In the answers to this question, Timothy Gowers asks:
I've been interested in this question for some time. I haven't put any serious thought into it, so all I can offer is a further question rather ...

**4**

votes

**3**answers

534 views

### What is the proper name for “compact closed” multiplicative intuitionistic linear logic?

Multiplicative intuitionistic linear logic (MILL) has only multiplicative conjunction $\otimes$ and linear implication $\multimap$ as connectives. It has models in symmetric monoidal closed ...