In sequent calculus, what's going on with sequents with multiple formulae in the succedent? 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.

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.