Questions tagged [linear-logic]
The linear-logic tag has no summary.
38 questions
8
votes
1
answer
569
views
Affine linear types
Is there an account of affine non-symmetric linear logic (ie with the weakening rule but not exchange or contraction) that treats the affine structure on its own merits and not just as a footnote?
It ...
- 9,296
3
votes
1
answer
130
views
Polarities for intuitionistic linear logic formulas inside classical linear logic (without linear implication)
In the article on intuitionistic linear logic on the LLWiki, it is stated that a polarization of formulas in classical linear logic is enough to make it equivalent to intuitionistic linear logic, ...
- 343
13
votes
3
answers
832
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 ...
- 639
4
votes
0
answers
202
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 $[-,-]$ ...
- 836
2
votes
1
answer
232
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
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 ...
- 5,033
5
votes
1
answer
256
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 ...
- 836
5
votes
0
answers
371
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 ...
- 836
2
votes
0
answers
129
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, ...
- 836
4
votes
0
answers
188
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 ...
- 836
5
votes
1
answer
258
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 ...
- 836
6
votes
1
answer
431
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 ...
- 836
5
votes
0
answers
142
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 ...
- 2,328
7
votes
1
answer
445
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
9
votes
1
answer
388
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 ...
- 69k