# How to derive ${ A \vdash C }$ from ${A \lor B \vdash C}$ in the sequent calculus LK?

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.

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}$$.

Finally:

$$\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}$$.

Finally:

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

• 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$. Jul 23, 2020 at 9:03
• 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? Jul 23, 2020 at 10:05
• @JuljaMuvv - Seq calculus proves sequents. We can always conjoin a finite set $S$ of fomulas into a single formula. Jul 23, 2020 at 10:49
• 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. Jul 23, 2020 at 12:50
• @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$ ? Jul 23, 2020 at 13:27