Stuck on rewriting logical implication

Question

I've started to work through Applied Mathematics for Database Professionals and have been stuck on one of the exercises for two days. I've been able to prove the expression: $$\left( P\Rightarrow Q \right) \Leftrightarrow \left( \neg Q \Rightarrow \neg P \right)$$ is true using a truth table but can't make the leap using rewrite rules.

Starting with the implication: $$ P \Rightarrow Q$$ Rewrite implication into disjunction: $$\neg P \vee Q $$ By commutativity the expression becomes: $$ Q \vee \neg P $$ Via double negation: $$ \neg \neg Q \vee \neg P $$ This is where I get stuck. The answer in the book shows rewriting the expression back into an implication: $$ \neg Q \Rightarrow \neg P $$ I understand where the $ \neg P $ comes from, it's from the initial rewrite rule. My confusion is, how is the $ \neg Q $ derived?

Answer 1

You apparently have a rule that allows you to go back and forth between $A\Rightarrow B$ and $\lnot A\lor B$. You’ve used it in the forward direction to go from $P\Rightarrow Q$ to $\lnot P\lor Q$, with $A=P$ and $B=Q$. Now use it in the reverse direction to go from $\lnot\lnot Q\lor\lnot P$ to $\lnot Q\Rightarrow \lnot P$ by taking $A=\lnot Q$ and $B=\lnot P$.

Answer 2

The rewrite rule says that $\lnot X \lor Y$ can be replaced by $X\Rightarrow Y$, and vice-versa.

In $\lnot\lnot Q \lor \lnot P$, let $X=\lnot Q$ and $Y=\lnot P$, and use the rewrite rule.