In sequent calculus, what's going on with sequents with multiple formulae in the succedent?

Question

The sequent proof systems I learned only allowed one formula on the right hand side of the sequent, and $\phi_1, \ldots, \phi_n \Rightarrow \psi$ (or ... $\vdash \psi$) is understood as saying that $\psi$ is a logical consequence of (or provable from) $\phi_1, \ldots, \phi_n$.

Now I'm seeing sequent calculus systems with right weakening:

$$\frac{\Gamma\vdash \Delta}{\Gamma\vdash \Delta,A} \text {RW}$$

So I guess $\Gamma\vdash \Delta,A$ has to be saying that at least one of $\Delta,A$ is provable from $\Gamma$ and not that both are. Why is this used?

I assume the notation has some payoff I'm missing, since it seems like sequences of wffs have different meanings based on whether they're in the antecedent or succedent.

Answer 1

The sequent calculus is based on the notation $\Gamma \Rightarrow \Delta$ (or $\Gamma \vdash \Delta$), with $\Gamma, \Delta$ finite (possibly empty) sequences of formulas, called a sequent.

The intuitionistic sequent calculus is obtained with the restriction that $\Delta$ consists of at most one formula.

For the semantics for sequents, see Gaisi Takeuti, Proof Theory (2nd ed - 1987), page 9:

intuitively a sequent $\gamma_1, \ldots, \gamma_m \vdash \delta_1, \ldots, \delta_n$ means :

"if $\gamma_1 \land \ldots \land \gamma_m$, then $\delta_1 \lor \ldots \lor \delta_n$".

Then we have [page 41] :

A sequent $\Gamma \vdash \Delta$ is satisfied [in an interpretation $\mathfrak I$] if either some formula in $\Gamma$ is not satisfied by $\mathfrak I$, or some formula in $\Delta$ is satisfied by $\mathfrak I$. A sequent is valid it it satisfied in every interpretation.