Cheap and Secure Web Hosting Provider : See Now

# [Solved]: Why do the sequent calculus NOT left and NOT right rules work?

, ,
Problem Detail:

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?

#### Answered By : Dave Clarke

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.

Question Source : http://cs.stackexchange.com/questions/12150

3.2K people like this