Why do the sequent calculus NOT left and NOT right rules work?

Question

The rules I am considering are $\frac{\neg A, \ \Gamma \implies \Delta}{\Gamma \implies \Delta, \ A} (\neg L)$ and $\frac{\Gamma \implies \Delta, \ \neg A}{A, \ \Gamma \implies \Delta} (\neg R)$

I am trying to get my head around some of the sequent calculus rules, and while I think I understand most of them, I am struggling to apply any intuition to the negation rules shown above.

The intuition of looking at the left as a conjunction of literals and the right as a disjunction of literals seems to break down, and I am unclear how to explain these rules to myself.

What is a sensible way to view such rules and put some understanding on them?

Answer 1

You could start by considering simplified versions of the rules and build intuition by considering those cases. For instance,

$$\frac{\neg A, \ B \implies C}{B \implies C, \ A} (\neg L)$$

can be interpreted as stating that $(\neg A\wedge B)\Rightarrow C$ implies $B\Rightarrow (C\vee A)$.

So if it is the case that $\neg A$ and $B$ are true implies $C$ is true, then if only $B$ is true, either $C$ is true (independently of $\neg A$) or $A$ is true, for otherwise $\neg A$ would be true, which combined with $B$ being true would make $C$ true.

A similar game can be played with the other case.

Answer 2

Applying your intuition, the premise of $(\neg L)$ is: under the hypotheses $\Gamma$, and assuming $A$ is wrong, then one of the conclusions $\Delta$ holds. So if I only know $\Gamma$, what can I conclude?

• Possibly $\Delta$ holds.
• If $\Delta$ doesn't hold, it can only be that the assumption that $A$ is wrong is not met. In other words, $\neg (\neg A)$ is true, which means that $A$ is true.

All in all, from the premise of $(\neg L)$, we get that $\Gamma$ entails $\Delta$ or $A$. That's the conclusion of $(\neg L).

Similarly, with $(\neg R)$: under the hypotheses $\Gamma$, either one of the conslusions $\Delta$ holds, or $\neg A$ holds. Now suppose that in addition to $\Gamma$ we know that $A$ is true. Then among the conclusions $\Delta, \neg A$, the item $\neg A$ cannot be true, because you can't have both $A$ and $\neg A$ (excluded middle). So it must be one (or more) conclusions in $\Delta$ that holds. All in all, $\Gamma$ and $A$ together entail $\Delta$, which is the conclusion of $(\neg R)$.

You'll note that $(\neg L)$ relies on the excluded middle. This rule does not hold in intuitionistic logic, where just because $\neg A$ leads to a contradiction doesn't mean you can prove $A$. $(\neg R)$ works in intuitionistic logic but might not in a fuzzy logic.