Sequent proof in propositional logic I've been struggling through this proof and I can't seem to arrive at the answer. I understand the rules and their applications. however, my intuition is of no help. Please help!
p → (q → r) ⇒(q∧~r)→~p
 A: General tip: I would almost always approach something like this by first writing the argument in prose, and then turning it into a formal derivation.  The two main things to get used to are making your prose proof detailed enough, and disentangling the mixture of top-down and bottom-up reasoning that one uses in prose to find the right order for the derivation.  For the level of detail in the prose proof — if you can’t see how to turn some step of it into one or two steps of sequent calculus, then try to rewrite that step of the prose proof to be more detailed.

So, back to the specific problem — first in prose, labelling the steps.
Our overall goal: assume $p$ implies that $q$ implies $r$; now we’re supposed to show that if $q$ holds and $r$ fails, then $p$ fails.
So, (A) assume additionally that $q$ holds and $r$ fails; now we just need to show that $p$ fails.
So (B) assume additionally that $p$ holds, and try to get a contradiction.  So to recap, our assumptions are:


*

*$p$ implies that $q$ implies $r$

*$q$ holds and $r$ fails

*$p$ holds


and we’re aiming for a contradiction.
(C) Putting (1) and (3) together, we get that $q$ implies $r$.  (D) But by (2), we also know $q$ holds, so by this and the previous step, $r$ holds.  (E) But (2) also tells us that $r$ fails; so this gives a contradiction!
Now, let’s turn this into a formal derivation!  Each labelled step above corresponds to one or two rule applications of sequent calculus.  The tricky bit is putting them in order.  (A) and (B) are “bottom-up” — they’re of the form “to prove our goal, do such-and-such”.  So they go at the end of the overall derivation: they’re $\to$-introduction steps, and they give a derivation from
$$(p \to (q \to r)),\ (q \land \lnot r),\ p \vdash \bot$$
to the overall goal.  (To see why (B) is a $\to$-introduction: remember that $\lnot p$ is an abbreviation for $p \to \bot$.)
Now steps (C)–(E) are “top-down”: they’re of the form “from our assumptions, we can do such-and-such”.  (C) uses $\to$-elimination (“we have $X \to Y$ and we have $X$, so we can get $Y$”); (D) uses that too, along with $\land$-elimination (to get $q$ from $q \land \lnot r$); and (E) uses these same ingredients again.
Hopefully you can fill in the details from here!
