The linear-logic tag has no usage guidance.

**0**

votes

**0**answers

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

**1**

vote

**0**answers

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

**4**

votes

**1**answer

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

**5**

votes

**1**answer

231 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

75 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: ...

**0**

votes

**0**answers

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

**5**

votes

**3**answers

246 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

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

**0**

votes

**1**answer

150 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

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

**3**

votes

**0**answers

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

**1**

vote

**0**answers

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

**7**

votes

**1**answer

343 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

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

**3**

votes

**3**answers

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