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.

$\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$ Mar 26, 2015 at 20:07

1 Answer 1

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.

$\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
    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
    Mar 26, 2015 at 21:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.