Soundness of cut in Gentzen's System LK

Question

I'm learning the sequent calculus in the classical setting (Gentzen's System LK), and I am a little confused about how to understand the soundness of Cut.

As I understand it, for a given sequent, we assume all of the antecedents to the left of $\vdash$, and conclude at least one of the consequents, per inclusive disjunction. For the following:

$$A,B \vdash C, D$$

We assume $A$ and $B$, and can merely conclude that exactly one of the following is true, but we don't know which: $C$, $D$, or ($C$ and $D$).

Now to Cut:

$$\frac {\Gamma \vdash A,\Delta \quad \quad \Gamma', A \vdash \Delta' } { \Gamma', \Gamma \vdash \Delta', \Delta }$$

If from the first premise ($\Gamma \vdash A,\Delta$), assuming $\Gamma$, we merely know that either $A$, $\Delta$, or ($A$ and $\Delta$), and we don't know which(!), how can we know that we're not dealing with the case that $\Delta$ is true and $A$ is not? How do we know that $A$ is satisfied for the second premise?

It seems to me that this would only be sound if we did something like taking $\Delta$ out of the picture:

$$\frac {\Gamma \vdash A \quad \quad \Gamma', A \vdash \Delta' } { \Gamma', \Gamma \vdash \Delta' }$$

In this case, we know from the first premise that $A$ must hold.

What am I misunderstanding? Thanks!

Answer 1

The things on top are both premises... we are given both of them. So we know that if $\Gamma$ holds then $A$ or $\Delta$ does (but not which one) and also that if $\Gamma'$ and $A$ hold, then $\Delta'$ holds. Note that both of these are conditional statements. We do not need to assume (or prove) that $A$ holds.

To see why the conclusion is sound given the premises, assume that $\Gamma$ and $\Gamma'$ both hold. We must show that either $\Delta$ holds or $\Delta'$ holds. Since $\Gamma$ holds, by the first premise, either $A$ or $\Delta$ holds. If $\Delta$ holds, we are done. If $\Delta$ doesn't hold, then $A$ holds. Then $\Gamma'$ and $A$ both hold, so by the second premise, $\Delta'$ holds.

Answer 2

There are various ways to intuit the semantics of a sequent. A different (but equivalent) interpretation of $A,B\vdash C,D$ would be:

It is impossible for all of $\neg A, \neg B, C, D$ to be false at the same time.

With this interpretation let us argue that if we know $\Gamma \vdash A, \Delta$ and $\Gamma', A \vdash \Delta'$, then $\Gamma, \Gamma' \vdash \Delta, \Delta'$.

Assume for a contradiction that $\neg\Gamma, \neg\Gamma', \Delta, \Delta'$ are all false.

By the first assumption $A$ cannot be false (since $\neg\Gamma$ and $\Delta$ are assumed false). By the second assumption $\neg A$ cannot be false (since $\neg\Gamma'$ and $\Delta'$ are assumed false). So $A$ cannot have any truth value, which is absurd.