I'd like to better understand the role of the contraction rule in Gentzen's $\mathsf{LK}$. I would like to have an example of a derivable sequent that is no longer derivable if the contraction rule is replaced by "derive $\Sigma, A \wedge B \vdash \Delta$ from $\Sigma, A ,B \vdash \Delta$ and "derive $\Sigma \vdash A \vee B , \Delta$ from $\Sigma \vdash A, B, \Delta$". I am particularly interested in the formulation of $\mathsf{LK}$ without the cut rule.
$\begingroup$
$\endgroup$
6
-
1$\begingroup$ 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?) $\endgroup$– Andrej BauerCommented Sep 9, 2016 at 6:19
-
$\begingroup$ $\Sigma$ and $\Delta$ are lists of formulas. $\endgroup$– Andre KornellCommented Sep 9, 2016 at 6:38
-
$\begingroup$ The statement of $\mathsf{LK}$ on wikipedia looks fine to me. $\endgroup$– Andre KornellCommented Sep 9, 2016 at 6:44
-
1$\begingroup$ 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? $\endgroup$– Andrej BauerCommented Sep 9, 2016 at 7:22
-
5$\begingroup$ 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. $\endgroup$– Emil JeřábekCommented Sep 9, 2016 at 10:10
|
Show 1 more comment