Trying to prove $p,p \to (r \to q) \vdash (\neg q \to \neg r)$ by using natural deduction.

Question

Inference rules allowed are: $\lor$, $\wedge$, $\rightarrow$, $\neg$ introductions and eliminations.

In question, it says I am allowed to make use of a lemma or equivalence as long as I provide a proof of it by natural deduction too. (I will come to that soon enough, hopefully.)

First of all, that "$,$" between $p$ and $p \rightarrow (r \rightarrow q)$ made me a bit confused, but I ended up assuming that comma just splits two premises we are given. I tried to not dig too much and proceeded to make proof, however I got stuck after using implication elimination on $p \rightarrow (r \rightarrow q)$ and obtaining $(r \rightarrow q)$. From there on, I have a sense that I will just use 4-5 more steps and reach $(\neg q \to \neg r)$ but I just couldn't figure it out.

Then I realized that I can make use of equation $p \rightarrow q \equiv \neg p \lor q $ .

As stated in question, I tried to prove this equation by natural deduction (I know at this point I am just making things harder than it is supposed to be, but what the heck..)

This is the proof I tried to make in fitch style:

Proof 1

If you realize I am using double negation here and I am not even sure if that is even allowed to use.

From here, I just needed to show that $(r \rightarrow q) \equiv (\neg q \rightarrow r)$ knowing $(\neg r \lor q) \equiv (\neg \neg q \lor \neg r)$ and that is $(\neg r \lor q) \equiv (q \lor \neg r)$

But if you realize, that means I will have to prove double negation law "$\neg \neg q \equiv q$" as well as commutative law "$(\neg r \lor q) \equiv (q \lor \neg r)$". Like these extra two small proofs are not enough, I also have to use them with proper notation/syntax in latex aside with fitch style proof tables.

This makes me realize that it is definitely a bad idea to make this proof by natural deduction using these "transformation" equivalences if I may call them that.

So, I think I need to give up on that idea and stick to direct proof with implications.

However, as stated above, I am stuck after implication elimination. Could you guys help me figure it out how to move forward from there?

P.S: Reason I state all those unnecessary steps is that, I think it is just more appropriate to not just "ask for a direct answer" but provide my thought process. Another challenge of doing this proof for me is that having to use fitch style proofs in latex. I just can't figure out where to place that "p" before comma in the question. Anyway, enough confusion!

Answer 1

In the Fitch system that I use, the proof is below. But again, your rules may be defined differently!

Answer 2

First, the theorem doesn't have any $\land$ or $\lor$ in it, so you won't need any inference using those (unless your negation rules are defined in terms of $\land$, some authors do that and it's a bit annoying).

Second, proving

$$p,~p\to(r \to q) \vdash \lnot q \to \lnot r$$

is the same as proving

$$p,~p\to(r \to q),~\lnot q \vdash \lnot r$$

And then applying $\implies$ introduction to move the $\lnot q$ to the right.

Try proving:

$$p,~p\to(r \to q),~\lnot q,~r \vdash \bot$$

And then use your $\lnot$ introduction rule to convert the $r \vdash \bot$ deduction into $\lnot r$. Depending on how your negation rules are set up (this isn't universal) you may be expected to prove $\dots,~r \vdash q \land \lnot q$ rather than $\dots,~r \vdash \bot$.