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:

enter image description here

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

In another case,

enter image description here

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:

enter image description here

Which even further blurs the distinction for me.


1 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.

  • 1
    $\begingroup$ much appreciated, thank you! $\endgroup$
    – dgan
    May 13 at 15:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.