Comma in turnstile (entailment)

A sequent $A_1, \dots, A_n \vdash B_1, \dots, B_m$ has to be intended as $A_1 \land \dots \land A_n \vdash B_1 \lor \dots \lor B_m$ (or equivalently, $\vdash (A_1 \land \dots \land A_n) \to (B_1 \lor \dots \lor B_m)$).

To remember that, in a sequent, the comma on left-hand side of the turnstile is a "and" and the comma on the right-hand side of the turnstile is a "or", you should recall the additive rule $\land_L^a$ for "and" on the left and the multiplicative rule $\lor_R^m$ for "or" on the right in classical sequent calculus LK:

\begin{align} \frac{\Gamma, A, B \vdash \Delta}{\Gamma, A\land B \vdash \Delta}\land_L^a & & \frac{\Gamma, \vdash A, B, \Delta}{\Gamma \vdash A\lor B, \Delta}\lor_R^m \end{align}

This is more than an analogy, because the two rules above are reversible i.e., for each of them, it is also the case that the premise is derivable in LK from the conclusion. So, the sequents $\Gamma, A, B \vdash \Delta$ and $\Gamma, A\land B \vdash \Delta$ are interderivable (i.e. from each of the two the other is derivable), and similarly the sequents $\Gamma, \vdash A, B, \Delta$ and $\Gamma \vdash A\lor B, \Delta$ are interderivable.


$$\bigvee_{i=0}^n \varphi_i \vdash \bigwedge_{j=0}^m\psi_j$$ can be reduced to showing whether $\varphi_i\vdash\psi_j$ for all $i\in\{0,\dots,n\}$ and $j\in\{0,\dots,m\}$. You can see this as a reflection of the facts $$(\varphi_1\lor\varphi_2)\to\psi\iff(\varphi_1\to\psi)\land(\varphi_2\to\psi)$$ and $$\varphi\to(\psi_1\land\psi_2)\iff(\varphi\to\psi_1)\land(\varphi\to\psi_2)$$ (The relation in terms of $\vdash$ is arguably more "fundamental" though.)

If we have a disjunction entailing a conjunction, we can "decompose" the entailment into simpler entailments not having those disjunctions and conjunctions, so that case is uninteresting. However, in general, we can't "decompose" a conjunction entailing a disjunction into simpler entailments. The notation reflects this fact. The "irreducible" sequents are the ones that have conjunctions entailing disjunctions.