# Questions tagged [linear-logic]

The linear-logic tag has no usage guidance.

36
questions

5
votes

2
answers

273
views

### What would you do with a new model of linear logic?

I have been working for some time with collaborators developing some models of linear logic which we are confident are new. However, none of us is deep enough in the field to answer the sceptic's ...

4
votes

0
answers

133
views

### Examples of $\ast$-autonomous $(\infty,1)$-categories

A $\ast$-autonomous category is a biclosed monoidal category together with a dualizing object. An object $\bot$ in a biclosed monoidal category $(\mathcal{C},\otimes)$ with left internal hom $[-,-]$ ...

2
votes

1
answer

156
views

### Semiring axioms which almost implement inverse, searching for domains other than lambda calculus

I'm working with an idempotent semiring which contains elements $C_i, \hat{C_i}$ with the following properties:
$$ {C}_i \hat{C_j} = 0 \quad\text{where}\quad i \neq j \quad\quad\quad\quad(\beta_0)$$
$$...

11
votes

2
answers

2k
views

### Can linear logic be used to resolve unexpected hanging/surprise examination paradox?

In the Unexpected Hanging Paradox, the prisoner tries to narrow down their date of execution using seemingly sound logical reasoning. They instead arrive at a contradiction. When the paradox is ...

4
votes

0
answers

114
views

### Full coherence for non-symmetric linearly distributive categories?

1. Context
Mac Lane's coherence theorem for monoidal categories can be phrased as "every formal diagram in a monoidal category commutes.“ I am interested in this type of coherence question for ...

4
votes

0
answers

319
views

### Is this linearly distributive category really free?

In Natural deduction and coherence for weakly distributive categories Blute et al. claim to give a presentation of the free (non-symmetric) linearly distributive category $\operatorname{PNet_E}(C)$ on ...

2
votes

0
answers

103
views

### Empires and the net criterion

Currently, I am struggling to understand the proof of Proposition 2.5 on page 250 (page 22 in the document) of the paper Natural deduction and coherence for weakly distributive categories by Blute, ...

4
votes

0
answers

133
views

### Correctness criteria for proof nets

In their paper Natural deduction and coherence for weakly distributive categories Blute, Cockett, Seely and Trimble introduce so-called proof circuits (aka two-sided proof structures) for the positive ...

5
votes

1
answer

196
views

### On the correspondence between proof nets and sequents

1. Context
While trying to answer my question on the existence of a (useful) graphical calculus for star-autonomous categories, I came across the paper Natural deduction and coherence for weakly ...

6
votes

1
answer

272
views

### Linear logic and linearly distributive categories

I asked this question ten days ago on MathStackexchange (see here). Despite having placed a bounty on the question, I have not received any answers or comments until now. Following Nick Champion's ...

5
votes

0
answers

106
views

### Equivalent formulation of linear logic with more axioms and less inference rules

We can formulate classical (sequent) logic with only the structural inference rules including cut, and a collection of axioms like $A, B \vdash A \wedge B$. This is equivalent to the usual sequent ...

7
votes

1
answer

340
views

### Ordered logic is the internal language of which class of categories?

Wikipedia says:
The internal language of closed symmetric monoidal categories is linear logic and the type system is the linear type system.
"A Fibrational Framework for Substructural and Modal ...

8
votes

1
answer

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

10
votes

0
answers

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

2
votes

2
answers

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

6
votes

0
answers

176
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

411
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

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

12
votes

1
answer

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

11
votes

1
answer

583
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

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

2
votes

0
answers

214
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

554
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

374
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

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

1
vote

0
answers

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

8
votes

3
answers

607
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

575
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

167
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

218
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

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

2
votes

0
answers

145
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), ...

6
votes

2
answers

685
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

420
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

949
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

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