Timeline for Injecting premises into two implicational premises connected by a tensor (multiplicative conjunction) in linear logic
Current License: CC BY-SA 3.0
3 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 26, 2015 at 21:53 | comment | added | Todd Trimble | 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$. | |
| Mar 26, 2015 at 20:56 | comment | added | Zerkezhi | 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. | |
| Mar 26, 2015 at 19:50 | history | answered | Todd Trimble | CC BY-SA 3.0 |