1
$\begingroup$

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: $B\multimap (D\multimap E)$

I originally hoped that I could simply reverse the tensor in (3) (making $(A\multimap B)$ and $(C\multimap D)$ individual premises), so I could inject the premises from (1) and (2). If that had been possible, I could have used assumed premises for (4) in order to use the conjunction elimination rule (which essentially states that I could replace the assumed $B$ and $D$ with $(B\otimes D)$ to derive E. Since I was told that this impossible, however, I am looking for another way to get to E, using the premises described above.

I hope that this question is less vague than my last one. If it is not, I apologise. I cannot see how I can make my question any clearer with my current level of knowledge in logic (or mathematical formalism).

I'm neither a logican nor mathematician; I'm currently looking into glue semantics, which uses Linear Logic to derive the meaning of a sentence. So I am grateful for any and all assistance.

Improve this question
$\endgroup$
1
  • $\begingroup$ Presentations of linear logic vary a bit; can you give a reference for what you are using? A rough answer: your approach sounds correct to me. It is not possible to get either one of $(A \multimap B)$ or $(C \multimap D)$ individually, but (in the presentations I know) inverting the tensor gives you the two of them together as formulas on the left of the $\vdash$, and you can then apply them to premises (1) and (2) as you describe. Some presentations may present this slightly differently, but something like this should always work. $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Mar 26, 2015 at 20:07

1 Answer 1

Reset to default
2
$\begingroup$

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 logic) is in $\ast$-autonomous categories, which are special symmetric monoidal closed categories, it will suffice to construct a morphism

$$A \otimes C \otimes [(A \multimap B) \otimes (C \multimap D)] \otimes (B \multimap (D \multimap E)) \to E \qquad (1)$$

using the language of smc categories. Using evaluation maps $A \otimes (A \multimap B) \to B$ and $C \otimes (C \multimap D) \to D$ together with associativity and symmetry isomorphisms, we easily get a morphism

$$A \otimes C \otimes [(A \multimap B) \otimes (C \multimap D)] \otimes (B \multimap (D \multimap E)) \to B \otimes D \otimes (B \multimap (D \multimap E)) \qquad (2)$$

and using similarly an evaluation $B \otimes (B \multimap (D \multimap E)) \to D \multimap E$ plus associativities, symmetries, we arrive at a morphism

$$B \otimes D \otimes (B \multimap (D \multimap E)) \to D \otimes (D \multimap E) \qquad (3)$$

and we compose $(2)$ and $(3)$ with an evaluation map $D \otimes (D \multimap E) \to E$ to get an arrow of type $(1)$.

I haven't seen your other question; I'll have a look.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Thanks, that's a great answer. One point of clarification: evaluation maps are considered universal, right? So it's not really a new premise introduced, specificly for this situation, but simply a way linear logic works, right? (like in classical logic, when we have "if A then B", "if B then C" ergo "if A then C") Anyway, this has helped a lot. I'll have to see how this interacts with the non-linear logic part of glue semantics, but that's trivial. $\endgroup$
    – Zerkezhi
    Commented Mar 26, 2015 at 20:56
  • $\begingroup$ Right, evaluation maps are universal. That has a technical meaning in category theory which essentially says $A \otimes -$ is left adjoint to $A \multimap -$, as mediated by "modus ponens" or evaluation $A \otimes (A \multimap B) \to B$. I would however draw a (not quite pedantic) distinction between internal composition $A \multimap B, B \multimap C \vdash A \multimap C$ and the cut rule which allows you to deduce, given $A \vdash B$ and $B \vdash C$, the conclusion $A \vdash C$. $\endgroup$
    – Todd Trimble
    Commented Mar 26, 2015 at 21:53

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .