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

Question

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.

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

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