Timeline for eliminating contraction
Current License: CC BY-SA 3.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 9, 2016 at 10:10 | comment | added | Emil Jeřábek | You can search for "substructural logic". The ultimate example is $A\vdash A\land A$. Note that without contraction, most connectives split into two. In the literature, $\land$ and $\lor$ are usually reserved for lattice conjunction and disjunction, using additive (shared-context) sequent rules. Multiplicative (split-context) conjunction, which is the one you defined in the question, tends to be denoted $\&$, $\cdot$, or $\otimes$; likewise, multiplicative disjunction is called $\oplus$. However, an incompatible notational convention was originally introduced for linear logic by Girard. | |
| Sep 9, 2016 at 8:39 | history | edited | Andre Kornell | CC BY-SA 3.0 |
added 1 character in body
|
| Sep 9, 2016 at 8:20 | comment | added | Andre Kornell | Yes, you are right; wikipedia has "sets" where it means "lists". | |
| Sep 9, 2016 at 7:22 | comment | added | Andrej Bauer | The Wikipedia formulation is broken. It says that $\Gamma$ and $\Delta$ are sets, but then it gives exchange and contraction as structural rules, which makes no sense for sets. Should we take $\Gamma$ and $\Delta$ to be lists, or should we ignore exchange and contraction? | |
| Sep 9, 2016 at 6:44 | comment | added | Andre Kornell | The statement of $\mathsf{LK}$ on wikipedia looks fine to me. | |
| Sep 9, 2016 at 6:38 | comment | added | Andre Kornell | $\Sigma$ and $\Delta$ are lists of formulas. | |
| Sep 9, 2016 at 6:19 | comment | added | Andrej Bauer | I think it would be good to be very precise about what you take as $\mathsf{LK}$, as little details here can matter. For instance, would the sequent calculus from Frank Pfenning's notes on sequent calculus be what you are looking for? (In particular, are $\Delta$ and $\Sigma$ sets or lists or multisets?) | |
| Sep 9, 2016 at 3:10 | history | edited | Andre Kornell | CC BY-SA 3.0 |
deleted 1 character in body
|
| Sep 9, 2016 at 2:58 | history | asked | Andre Kornell | CC BY-SA 3.0 |