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