Suppose $\Gamma\vdash\lnot (A\to B)$. How do I show that both $\Gamma\vdash A$ and $\Gamma\vdash \lnot B$ using sequent calculus inference rules?

Here is my attempt to obtain $\Gamma\vdash A$: From $\Gamma\vdash\lnot (A\to B)$, I can obtain $A\to B,\Gamma\vdash$ using $\lnot$L rule and the cut rule using process outlined in this answer. The sequent $B\vdash B,A\to B$ is easily derivable. After applying the cut rule to both $A\vdash A,A\to B$ and $A\to B,\Gamma\vdash$, we get $\Gamma,A\vdash A$...

What are next steps should I take?


1 Answer 1


From axiom $A \vdash A$ derive $A \vdash A,B$ by $(\text {Weak})$and then $\vdash A \to B,A$. Using $(\lnot \text L)$ we get: $\lnot (A \to B) \vdash A$ and we are ready for $(\text {Cut})$.

The same starting from $B,A \vdash B$ to $B \vdash A \to B$ from which $\lnot (A \to B) \vdash \lnot B$.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .