Sequent calculus and vs comma: $a \land b \implies ...$ vs $a, b \implies ...$

Question

I was reading "Open Logic book", "Sequent Calculus". Given the fact that all antecedents must hold for at least one succedent to hold, I can't get rid off the impression that using a "comma" on the left side doesn't bring anything new, and I could simply replace it with "$\land$".

For example, let's take:

What prevents me from treating the bottom part as if it was "$-\varphi \land \Gamma \implies \Delta$"?

In another case,

Here "$\psi$" is introduced out of thin air, and is "$\land$-appended" to existing context. Which looks extremely similar to "weakening-left" rule which also introduces a new proposition out of nothing, but now prepending it with a comma:

Which even further blurs the distinction for me.

Answer 1

What prevents me from treating the bottom part as if it was "$-\varphi \land \Gamma \implies \Delta$"?

Nothing prevents you! In fact, this is exactly the right idea. You can think of the symbols in sequent calculus as follows:

• comma on the left means $\land$
• comma on the right means $\lor$
• $\implies$ means $\to$ (if then)

In fact, we could go further: we could develop all the rules of sequent calculus using only $\land$ and $\lor$ in place of commas The negation left rule, for example, would look like this: from the formula $\Gamma \to \Delta \lor \varphi$, deduce $\Gamma \land \lnot \varphi \to \Delta$.

So why don't we do it that way? There are a few reasons:

• First and most importantly, using meta-symbols gives us the following property: each logical symbol can only be introduced by the introduction rules for that symbol, and by no other rules. If comma were not a meta-symbol, then for example, the negation left-introduction rule would remove the symbol $\lor$ and add the symbol $\land$. This would defeat the whole point of sequent calculus: to give an account of each logical operator alone in isolation, without reference to the other logical operators. The goal is to give every logical operator a meaning solely in terms of the syntax of commas and $\implies$.

• A second key property of sequent calculus is that a logical symbol (like $\land$ and $\lor$) can only ever be introduced, and never taken away. So we use commas for the meta-symbols since they can be both introduced and taken away (and also reordered).

• Another advantage of comma is that it reveals a fundamental symmetry between conjunction $\land$ on the left, and disjunction $\lor$ on the right, since they are both represented by comma. It shows that, for example, the left-rules for conjunction match the right-rules for disjunction and vice versa; this wouldn't be clear if we didn't use the same symbol for both.

In summary: yes, comma is just conjunction on the left and disjunction on the right! But it's used as a meta-symbol, rather than a symbol in the logic itself, and this has very important implications. Using meta-symbols is what allows us to claim sequent calculus is a structural, syntactic theory of proofs and not just an arbitrary collection of rules about semantic implication.