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

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.

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.

• much appreciated, thank you!
– dgan
May 13 at 15:57