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

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!

• @Arthur This is natural deduction, not binary logic. – DanielV Oct 30 '16 at 13:59
• Different authors use different axioms for $\lnot$ and $\bot$ in natural deduction. It would help to list yours explicitly. – DanielV Oct 30 '16 at 14:09
• @Anonymous $\vdash$ is entailment. From a logical point of view, $A \vdash B$ means $B$ is provable from $A$. From a programming point of view, $A \vdash B$ means "if $A$ is in theory, then $B$ can be added to the theory". – DanielV Oct 30 '16 at 15:43
• $\Gamma \vdash \phi$ means that statement $\phi$ can be derived from the set of statements $\Gamma$. Of course, whether it can be derived or not really depends on what derivation rules you have or don't have, so you really should say something like $\Gamma \vdash_S \phi$ to say that $\phi$ can be derived from $\Gamma$ using the formal proof system $S$. But since we typically assume that we are using a sound and complete proof system, we drop the $S$. – Bram28 Oct 30 '16 at 15:45
• @Anonymous No, absolutely not!! You are mixing logical operators with metalogical expressions about statements that involve logical operators! – Bram28 Oct 30 '16 at 15:58

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

• This is proof by contradiction, am I right? Also thanks. (Which "editor" is that you are using btw?) – Bonellia Oct 30 '16 at 15:37
• Yes, the $\neg$ Intro rule shows that the assumption of $R$ leads to a contradiction, so $R$ is not true. The $\neg$ Intro thus formalizes the Proof by Contradiction kind of reasoning. I use a program called Fitch, which is part of a software package that comes with the book "Language, Proof, and Logic" – Bram28 Oct 30 '16 at 15:39
• This isn't proof by contradiction. Proof by contradiction requires double negation elimination. Proof by contradiction is $(\lnot C \vdash \bot) \vdash C$, this is $(C \vdash \bot) \vdash \lnot C$. – DanielV Oct 30 '16 at 15:41
• There is a problem in this proof by the way, which is using "$\bot$ Intro". This is not allowed. Trying to find a workaround myself atm :/ – Bonellia Oct 30 '16 at 15:44
• @Bonellia It is allowed in the system I use (notice all the checkmarks :) ) ... but like I said, the system you use maybe different. So, again, what are your rules? – Bram28 Oct 30 '16 at 15:47

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$.

• Sorry for the silly remark, but I think I need some sort of "English" translation to "$,$" in order to completely understand what I am trying to prove here. When I see "$\rightarrow$" I can tell "implies that" or when I see "$\vdash$" I can tell "x ⊢ y means y is provable from x" (with words used specifically in wikipedia) or just say "therefore". But that comma doesn't translate to anything in my mind. What would you come up with to explain meaning of that ","? I tried to check my books, pdfs, notes etc but since it is a single character, I can't really refer to it, so searches fail. – Bonellia Oct 30 '16 at 14:09
• @Bonellia Comma is used to indicate multiple statements. So $a,~b\vdash c,~d$ means "the two statements, $c$, $d$, are provable from the two statements, $a$, $b$". – DanielV Oct 30 '16 at 15:18