How to derive ${ A \vdash C }$ from ${A \lor B \vdash C}$ in the sequent calculus LK? It seems obvious that if ${A \lor B \vdash C}$ is true, then ${ A \vdash C }$ is true. There are rules

$\cfrac {\qquad A, \ \Gamma \ \rightarrow \ \Delta }{\ A \land B, \ \Gamma \ \rightarrow \ \Delta \ }$, $\cfrac {\qquad B, \ \Gamma \ \rightarrow \ \Delta}{\ A \land B, \ \Gamma \ \rightarrow \ \Delta \ }$ $\cfrac {\Gamma \ \rightarrow \ \Delta, \ A \qquad \Gamma \ \rightarrow \ \Delta, \ B}{\ \qquad \ \Gamma \ \rightarrow \ \Delta, \ A\land B \ }$ $\cfrac {A, \ \Gamma \ \rightarrow \ \Delta \qquad B, \ \Gamma \ \rightarrow \ \Delta \ }{\ A \lor B, \ \Gamma \ \rightarrow \ \Delta \ \qquad}$, but they cannot be used here.


1 Answer 1


From axiom and $\lor$-r: $\cfrac { \ A \vdash A}{\ A \vdash A \lor B }$ Assumption: $A \lor B \vdash C$. Then apply Cut to get $A\vdash C$.

Without $\text {Cut}$ [and without proper tree formatting...]:

  1. right branch:

$\cfrac { \ C \vdash C }{\ A, C \vdash C }$, by Ax and Weak, then:

$C \vdash A \supset C$, by $\supset \text {-r}$.

  1. left branch:

$\cfrac { \ A \vdash A }{\ A \vdash A, C }$, by Ax and Weak, then:

$A \vdash A \lor B, C$, by $\lor \text {-r}$, then:

$\vdash A \lor B, A \supset C$, by $\supset \text {-r}$.


$\cfrac { \vdash A \lor B, A \supset C \qquad C \vdash A \supset C }{ A \lor B \supset C \vdash A \supset C }$, by $\supset \text {-l}$.


$\vdash (A \lor B \supset C) \supset (A \supset C)$, by $\supset \text {-r}$.

  • $\begingroup$ Thank you. How about Cut-elimination theorem? Doesn't it say that it can be derived without using Cut-rule? Sorry, maybe this theorem has nothing to do with it and I just confuse the question by mentioning it. But I've seen in some books lists of rules of sequent calculus where no Cut-rule was. And I wonder how they suppose to derive $A \rightarrow C$ from $A \lor B \rightarrow C$. $\endgroup$
    – Julja Muvv
    Jul 23, 2020 at 9:03
  • $\begingroup$ It means that we can avoid using Cut only when the derivation is from the empty set (so we have the tautology as a result), but not when we use derivation to prove that $S \vDash s$, where $S$ is a set of sequents, $s$ is a sequent? $\endgroup$
    – Julja Muvv
    Jul 23, 2020 at 10:05
  • $\begingroup$ @JuljaMuvv - Seq calculus proves sequents. We can always conjoin a finite set $S$ of fomulas into a single formula. $\endgroup$ Jul 23, 2020 at 10:49
  • $\begingroup$ Let $p$, $q$, $r$ be variables. As you show in the first edit of the answer, we can derive ${ p \vdash r }$ from ${p \lor q \vdash r}$ using Cut. But in the new answer you derive ${\vdash (p \lor q \rightarrow r}) \rightarrow ({ p \rightarrow r } )$, not ${ p \vdash r }$ from ${p \lor q \vdash r}$. It's not the same problem. I try to understand if we can exactly derive ${ p \vdash r }$ from ${p \lor q \vdash r}$ without Cut, like you did it with Cut. And if we can't, why not. $\endgroup$
    – Julja Muvv
    Jul 23, 2020 at 12:50
  • 1
    $\begingroup$ @JuljaMuvv - I think not, in the form you have written it. Sequent calculus proves sequents and by soundness to be provable a sequent must be a tautology: $p \to r$ is not. Having said that, all rules - except Cut - add connectives and no rule remove it: so, how the "unpack" $p \lor q$ ? $\endgroup$ Jul 23, 2020 at 13:27

You must log in to answer this question.

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