# How to prove this type of equivalence?

Show that from: $P \ \rlap\Leftarrow\Rightarrow Q$.

It follows that: $(P \Rightarrow R)\, \rlap\Leftarrow\Rightarrow (Q \Rightarrow R)$

I don't understand where the $R$ suddenly came from? I try to use these rules as a reference.

-
You should imagine the word "if" somewhere: If $(P\implies R)$ we have $(Q\implies R)$ and vice versa. – gebruiker Jun 8 '14 at 14:48

\begin{align} P \iff Q &\equiv \lnot P \iff \lnot Q \\ \\ [\lnot P \iff \lnot Q]&\implies [(\lnot P \lor R) \iff (\lnot Q \lor R)]\\ \\ & \equiv (P\rightarrow R)\iff (Q\rightarrow R)\end{align}

-
Wow thanks. I understand that! Ah man, I need to practice this a LOT.. – user3125591 Jun 8 '14 at 14:57
You're welcome! It gets easier, with practice! – amWhy Jun 8 '14 at 15:03
I believe you mean to use implication instead of equivalence...consider $$\bigg(P \iff Q \bigg) \equiv \bigg( (P \Rightarrow R) \iff (Q \Rightarrow R)\bigg)$$ for $P$, $\lnot Q$, and $R$. $$\bigg(\top \iff \bot \bigg) \equiv \bigg( (\top \Rightarrow \top) \iff (\bot \Rightarrow \top)\bigg)$$ $$\bot \equiv \bigg( \top \iff \top\bigg)$$ $$\bot$$ – DanielV Jun 8 '14 at 15:05
Thanks, @DanielV. I replaced equivalence with implication at the one crucial spot. – amWhy Jun 8 '14 at 15:11
@amWhy Thanks, I'd be interested what your justification is for the implicative step. Although we all intuitively know it is true, I'm not so sure that the logic of the linked PDF properly defends that transition. – DanielV Jun 8 '14 at 16:08

You have linked an attachment with "some rules" but I'm expecting that you know also about inference rules, like $\Rightarrow$-elimination (modus ponens) and $\Rightarrow$-introduction [see Gordon J. Pace, Mathematics of Structures for Computer Science (2012), page 34].

Also transitivity of implication [page 35] is useful :

$(P ⇒ Q) \land (Q ⇒ R) \vdash P ⇒ R$.

Having these rules at your disposal, you can "unpack" $P \Leftrightarrow Q$ into $(P \Rightarrow Q) \land (Q \Rightarrow P)$.

Thus, by $\land$-elimination, we have :

$P \Leftrightarrow Q \vdash P \Rightarrow Q$

$P \Leftrightarrow Q \vdash Q \Rightarrow P$.

Then, from $P \Rightarrow R$ and $Q \Rightarrow P$, by transitivity you may have :

$(Q \Rightarrow P), (P \Rightarrow R) \vdash Q \Rightarrow R$

and by $\Rightarrow$-introduction conclude with :

$Q \Rightarrow P \vdash (P \Rightarrow R) \Rightarrow (Q \Rightarrow R)$.

In the same way, we have :

$P \Rightarrow Q \vdash (Q \Rightarrow R) \Rightarrow (P \Rightarrow R)$.

Thus, by $⇔$-introduction [page 38] :

$(P \Rightarrow Q), (Q \Rightarrow P) \vdash (P \Rightarrow R) \Leftrightarrow (Q \Rightarrow R)$.

Putting all together :

$P \Leftrightarrow Q \vdash (P \Rightarrow R) \Leftrightarrow (Q \Rightarrow R)$.

-
Thank you very much! – user3125591 Jun 8 '14 at 17:56

This is a bit more of an involved question that it seems at first glance. Define (T1) as $$P \Rightarrow Q \tag{T1}$$ and define (T2) as $$(P \Rightarrow R) \iff (Q \Rightarrow R) \tag{T2}$$

First, if you are trying to prove $T_1 \equiv T_2$, you are going to have trouble because it's not true, a counter example is $P$, $\lnot Q$, and $R$.

Second, if you are trying to prove $T_1 \vdash T_2$, while a sound statement, you are still going to have trouble. $\vdash$ roughly means "it follows from your logical rules of inference". Look at the logical rules of inference on your linked PDF. They are all of the form $\text{this} \equiv \text{that}$. But since we've already established that you can't infer $T_1 \equiv T_2$ (assuming your linked PDF is sound) then no application of the rules in the PDF can give us $T_1 \vdash T_2$.

What you can do, if you are bound to the logic of your PDF, is to prove $$T_1 \Rightarrow T_2 \equiv \text{true}$$

This is still a bit tricky since your PDF doesn't specify whether $\equiv$ means that replacement can be done inside an expression, or whether the rule has to applied to the whole expression. But because there aren't any rules where $\iff$ exists not as the root function of the transform, we have to assume internal replacement is possible, otherwise a proof doesn't exist within the logic of the PDF.

I don't think there is much to learn from actually tediously figuring out which rules of inference give your equation, so I'll just point out some observations about the PDF:

• It seems to be missing a rule that $P \lor \lnot P \equiv \text{true}$, and I can't seem to figure out how to make one...
• Many of the rules of the PDF are redundant
• Working in a logic that only admits equivalences can be fun and enlightening, but is not recommended for a beginner, I strongly recommend a different reference
-
Thank you for the comment and advice, I really appreciate it! – user3125591 Jun 8 '14 at 16:40

One way to see this is with the method of analytic tableaux, since you can pull $P\leftrightarrow Q$ out from $P\leftrightarrow Q\vdash ((P\to R)\leftrightarrow(Q\to R))$ and just show $\vdash (P\leftrightarrow Q)\to ((P\to R)\leftrightarrow(Q\to R))$. That boils down to showing $$(P\leftrightarrow Q)\to ((P\to R)\leftrightarrow(Q\to R))\tag{1}$$ is a tautology. You apply a series of contradiction-hunting rules to the negation of $(1)$ to get a tableau, like so

,

which is closed (i.e., each path ends in a contradiction), meaning that $(1)$ was indeed a tautology.

Can you complete the tableau? (There's a hint below.)

It continues after the $?$ in the exact same way it does after $P\to R$, mutatis mutandis.

See the Handbook of Tableau Methods for a precise, detailed account of this approach.

I hope that helps :)

-
One disadvantage with this method is that it obscures which rules are being used and when; it's great for computation and for getting a feel for why theorems hold, but not for understanding the rules. So maybe this answer wasn't what you were after. I'm sorry. – Shaun Jun 10 '14 at 18:39