Comma in turnstile (entailment)

Question

In a sequent, on the left and right-hand side of the turnstile operator, does the comma denote disjunction or conjunction?

$$\frac{...}{\Delta_1,\Delta_2 \vdash \Gamma_1,\Gamma_2}$$

I think it's one of the following, but I can never remember which:

• $\Delta_1$ and $\Delta_2$ entails $\Gamma_1$ or $\Gamma_2$, or
• $\Delta_1$ or $\Delta_2$ entails $\Gamma_1$ and $\Gamma_2$?

Answer 1

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.

Answer 2

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

Answer 3

In presence of structural rules, comma on left denotes conjunction and comma on right denotes disjunction. However, in absence of structural rules, conjunction and disjunction split and we need other operators, namely fusion, and fission.
What I want to emphasize is to note that only logical rules cannot interpret our syntax in sequent-calculus and structural rules are not just to manipulate sequents, they have logical content and they help to interpret the operators.