17
votes

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

It's been some years since I updated my comprehensive bibliography on the surprise examination or unexpected hanging paradox, but I'm pretty sure there's no published paper that tries to enlist linear ...

- 68.5k

13
votes

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

Here is why this won't work.
Consider the following "paradox":
I tell my class that "tomorrow, we will have a surprise exam. I promise that you will not know about this exam until you ...

- 21.2k

6
votes

Accepted

### Linear logic and linearly distributive categories

Yes, Cockett and Seely's comment about proof theory is a reference to the theory/category adjunction. Each kind of theory corresponds to a kind of category, for instance:
Theory
Category
simply ...

- 61k

6
votes

Accepted

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

Yes, ordered logic is the internal language of non-symmetric monoidal categories. As with linear and nonlinear logic, if the ordered logic contains function-types then they correspond to internal-...

- 61k

6
votes

### Embedding of classical into intuitionistic linear logic

There are actually many negative translations of classical linear logic into intuitionistic linear logic, just as there are many negative translations of classical logic into intuitionistic/minimal ...

- 3,103

6
votes

Accepted

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

This is (a piece of) Proposition 3.8 in
Harold Schellinx, Some Syntactical Observations on Linear Logic, J. Logic Compututa., Vol. 1 No. 4, pp. 537-559, 1991. (pdf at oxford journals)
His proof-...

- 3,103

6
votes

Accepted

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

Your notation is a bit confusing because usually in linear logic and related systems $\top$ denotes the unit of additive conjuction (i.e., categorically, the terminal object), but then when you ...

- 1,306

6
votes

Accepted

### Is Girard's LU just an embedding of classical and intuitionistic logic into linear logic?

Sorry if my answer comes so late, maybe you already figured it out by yourself in the meantime, I hope this helps anyway.
I think the main misunderstanding is that the "non-chimeric" fragment of $\...

- 1,306

6
votes

Accepted

### Dioperads vs polycategories

In Martin Markl's article "Operads and PROPs," just after Def. 64, the dioperad-polycategory connection is briefly mentioned. Markl attributed this observation to Leinster.
In my book with Mark W. ...

- 456

2
votes

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

The beginnings of a connection have been made, but there is still quite a bit left to do. The key is to formulate data types as polynomial functors.
The history of polynomial functors is very well ...

2
votes

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

Well, this is very easy, but because linear logic might be considered a little too specialized for Mathematics StackExchange, I'll answer.
Since the natural semantics of MLL (multiplicative linear ...

- 51k

2
votes

### Distributivity of ! over?

I would tend to say "no".
However, besides my comment above, which is not very pertinent, let me mention the paper Combining effects and coeffects via grading, by Marco Gaboardi, Shin-ya Katsumata, ...

- 1,306

1
vote

### On the correspondence between proof nets and sequents

First, it might be of interest to you to know that Table 1 in this paper by Dominic Hughes compares various diagrammatic presentations of the free *-autonomous category (including the paper you've ...

1
vote

Accepted

### What is the sequent calculus for differential linear logic?

Although this is well-known to experts, it is surprisingly difficult to find a paper explicitly presenting the sequent calculus of (classical) differential linear logic (DiLL). The following one is a ...

- 1,306

1
vote

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

So-called relational semantics of linear logic is usually regarded as a denotational semantics reflecting the resource-sensitiveness of the system.
Every type A is interpreted as a set $[\![A ]\!]$, ...

Only top scored, non community-wiki answers of a minimum length are eligible

#### Related Tags

linear-logic × 33lo.logic × 21

ct.category-theory × 11

monoidal-categories × 7

proof-theory × 6

reference-request × 4

computer-science × 4

lambda-calculus × 4

string-diagrams × 3

graph-theory × 2

type-theory × 2

categorical-logic × 2

intuitionism × 2

linear-algebra × 1

ac.commutative-algebra × 1

mp.mathematical-physics × 1

computability-theory × 1

topos-theory × 1

quantum-mechanics × 1

mathematical-philosophy × 1

operads × 1

braided-tensor-categories × 1

modal-logic × 1

coherence × 1

paradox × 1