# Tag Info

Accepted

### What is the intuition behind linear logic?

I'm not sure this question is ideal for CSTheory, but given that it's already gathering upvotes, here is an answer somebody might have given had the question been posted on cs.stackexchange. In ...
• 11.5k

### How does linear logic achieve resource management?

The following answers your first two questions. It seems to me that you're working under the assumption that propositional linear logic is a 4-valued logic, in the same sense that propositional ...
• 5,493

### How to think about coherent spaces intuitively?

I always had trouble forming an intuition for coherence spaces, until I became more familiar with domain theory and read Girard's "The System F of variable types, fifteen years later". ...
Accepted

### Can you assign a type to any term of the λEA-calculus?

For question 1, the answer is no, and is no for almost any type discipline (except certain intersection types): the fact that a term is (strongly or weakly) normalizable does not imply in general that ...
• 5,493
Accepted

### Recursive types and the empty type

First, note that nothing turns on the presence or absence of the empty type: if you have a nonlinear calculus with function types and unrestricted recursive types, then it is inconsistent. Indeed, ...
• 32.6k
Accepted

### Parametricity of Linear Logic

Various people are interested in proving this sort of thing. Neel Krishnaswami mentioned this particular theorem here. I’ve also seen Frank Pfenning give some cool examples for ordered logics. For ...
• 225
Accepted

### A stronger multiplexing rule for soft linear logic?

Your rule $(\ast)$ is sometimes referred to as "absorption". I think the first who considered it was Jean-Marc Andreoli in his paper on focusing proofs. Indeed, it makes a lot of sense in proof ...
• 5,493

### Algebraic account of Gaussian elimination?

You really should read Gowers' essay carefully - it cleanly details the reasons why you need a basis in general. So if there is going to be an algebraic account of Gauss-Jordan, it will necessarily ...
• 1,540

### Why does this cut elimination procedure terminate (contraction case)?

I extend what I wrote as a comment. As there is a great number of cases in the proof, I only give an idea of why this transformation terminates. The short answer is: In the case promotion vs ...
• 2,174
Accepted

### Does this variant of Multiplicative Linear Logic with mix rule enjoy cut elimination?

For question 1, if by "deadlock" you mean "non-trivial vicious circle", then the answer is obviously yes, simply because a non-trivial vicious circle cannot be typed: you will have a cut between a ...
• 5,493
Accepted

### Is the set of Multiplicative Proof Nets a proper subset of set of well formed single-agent Interaction Nets?

Your observation about cut-elimination being faithfully represented in the unlabelled interaction nets is correct. However, the answer to your question is no. Let us call $\delta$ the unique agent ...
• 5,493
Accepted

### Which are the rules for minimal logic in both sequent calculus and natural deduction styles?

The first book that Andrej Bauer suggested above (Basic Proof Theory) contains the rules you are looking for. Due to the connection between minimal logic and lambda-calculus, the following paper might ...
• 307

### A stronger multiplexing rule for soft linear logic?

Here is a partial answer: the rule $(*)$ is not conservative over SLL. Indeed, McKinley showed that soft linear set theory with unrestricted comprehension is nontrivial — but adding $(*)$ makes ...
• 675