patternMinor
Why do the sequent calculus NOT left and NOT right rules work?
Viewed 0 times
leftwhythesequentcalculusworkandrulesnotright
Problem
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?
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?
Solution
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.
$$\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.
Context
StackExchange Computer Science Q#12150, answer score: 6
Revisions (0)
No revisions yet.