Questions tagged [linear-logic]
The linear-logic tag has no usage guidance.
34
questions
14
votes
1
answer
946
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 ...
- 9,003
12
votes
1
answer
717
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;\...
- 64.1k
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,752
11
votes
1
answer
574
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 ...
- 64.1k
10
votes
0
answers
356
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 ...
- 397
8
votes
3
answers
591
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$, ...
- 951
8
votes
1
answer
321
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 ...
- 64.1k
7
votes
1
answer
334
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 ...
- 261
7
votes
1
answer
418
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 ...
- 173
6
votes
2
answers
681
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 $\...
- 951
6
votes
1
answer
371
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 ...
- 2,746
6
votes
1
answer
255
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 ...
- 594
6
votes
1
answer
410
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 ...
- 121
6
votes
0
answers
168
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 ...
- 9,003
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) = ...
- 64.1k
5
votes
1
answer
538
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 ...
- 2,746
5
votes
1
answer
194
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 ...
- 594
5
votes
0
answers
104
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 ...
- 779
4
votes
3
answers
574
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 ...
- 581
4
votes
3
answers
660
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 ...
- 1,532
4
votes
0
answers
113
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 ...
- 594
4
votes
0
answers
318
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 ...
- 594
4
votes
0
answers
131
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 ...
- 594
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
2
answers
381
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.
- 33
2
votes
1
answer
149
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)$$
$$...
- 225
2
votes
0
answers
100
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, ...
- 594
2
votes
0
answers
213
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 ...
- 121
2
votes
0
answers
143
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), ...
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\...
- 21
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 ...
- 21
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\ |\ ...
0
votes
1
answer
159
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?
