# Proof of equivalence theorem using equational calculus

I have to show the following theorem:

$p\vee \neg p \equiv ((p \vee q)\wedge \neg (\neg p \wedge (\neg q \vee \neg r)))\vee (\neg p \wedge \neg q) \vee (\neg p \wedge\neg r)$

I have proved

$((p \vee q)\wedge \neg (\neg p \wedge (\neg q \vee \neg r)))\vee (\neg p \wedge \neg q) \vee (\neg p \wedge\neg r) \implies p\vee \neg p$

It is true because we apply the definition of the implication, then we have:

$[((p \vee q)\wedge \neg (\neg p \wedge (\neg q \vee \neg r)))\vee (\neg p \wedge \neg q) \vee (\neg p \wedge\neg r)] \vee (p\vee \neg p)$

By applying the negation rule, we have:

$[((p \vee q)\wedge \neg (\neg p \wedge (\neg q \vee \neg r)))\vee (\neg p \wedge \neg q) \vee (\neg p \wedge\neg r)] \vee (true)$

And finally, by using the dominance rule of OR, we have:

$true$

BUT I have not been able to solve the other way:

$p\vee \neg p \implies ((p \vee q)\wedge \neg (\neg p \wedge (\neg q \vee \neg r)))\vee (\neg p \wedge \neg q) \vee (\neg p \wedge\neg r)$

I have tried with this:

$\Big \langle \implies definition \Big \rangle$

$\Big \langle DeMorgan, and \wedge negation \Big \rangle$

$false \vee ((p \vee q)\wedge \neg (\neg p \wedge (\neg q \vee \neg r)))\vee (\neg p \wedge \neg q) \vee (\neg p \wedge\neg r)$

$\Big \langle \vee identity \Big \rangle$

$((p \vee q)\wedge \neg (\neg p \wedge (\neg q \vee \neg r)))\vee (\neg p \wedge \neg q) \vee (\neg p \wedge\neg r)$

$\Big \langle \wedge/\vee distribution \Big \rangle$

$((p \vee q)\wedge \neg (\neg p \wedge (\neg q \vee \neg r)))\vee (\neg p \wedge (\neg q \vee \neg r))$

That's my solution progress up to this moment.

Some suggestions, tips, etc.?

$$[((p∨q)∧¬(¬p∧(¬q∨¬r)))∨(¬p∧¬q)∨(¬p∧¬r)]∨(p∨¬p) \\ [((p∨q)∧(p∨(q∧r)))∨(¬p∧¬q)∨(¬p∧¬r)]∨(p∨¬p) \\ [((p∨q)∧((p∨q)∧(p∨r)))∨(¬p∧¬q)∨(¬p∧¬r)]∨(p∨¬p) \\ [((p∨q)∧(p∨q)∧(p∨r))∨(¬p∧¬q)∨(¬p∧¬r)]∨(p∨¬p) \\ [((p∨q)∧(p∨r))∨(¬p∧¬q)∨(¬p∧¬r)]∨(p∨¬p) \\ [(p∨(q∧r))∨(¬p∧¬q)∨(¬p∧¬r)]∨(p∨¬p) \\ (q∧r)∨(¬p∧¬q)∨(¬p∧¬r)∨(p∨¬p) \\ (q∧r)∨(¬p∧(¬q∨¬r))∨(p∨¬p) \\ (q∧r)∨(¬p∧¬(q∧r))∨(p∨¬p) \\ (((q∧r)∨¬p)∧((q∧r)∨¬(q∧r)))∨(p∨¬p) \\ (q∧r)∨¬p∨(p∨¬p) \\ (q∧r)∨(p∨¬p) \\ (q∧r)∨true \\ s∨true \\ true \\ (p∨¬p)$$
reverse that up and put a $≡$ between each two lines.
The simplest way of solving this, is to treat it as a simplification problem. And here it seems most appropriate to simplify both sides separately, using the basic laws of logic.\newcommand{\calc}{\begin{align} \quad &} \newcommand{\op}[1]{\\ #1 \quad & \quad \unicode{x201c}} \newcommand{\hints}[1]{\mbox{#1} \\ \quad & \quad \phantom{\unicode{x201c}} } \newcommand{\hint}[1]{\mbox{#1} \unicode{x201d} \\ \quad & } \newcommand{\endcalc}{\end{align}} \newcommand{\Ref}[1]{\text{(#1)}} \newcommand{\then}{\Rightarrow} \newcommand{\when}{\Leftarrow} \newcommand{\true}{\text{true}} \newcommand{\false}{\text{false}}
The left hand side is immediately equivalent to $\;\true\;$, by the law of the excluded middle. The right hand side we simplify as follows: $$\calc \tag{RHS} \Big((p \lor q) \land \lnot \big(\lnot p \land (\lnot q \lor \lnot r)\big)\Big) \;\lor\; (\lnot p \land \lnot q) \lor (\lnot p \land \lnot r) \op\equiv\hint{left part: simplify using DeMorgan} \Big((p \lor q) \land \big(p \lor (q \land r)\big)\Big) \;\lor\; (\lnot p \land \lnot q) \lor (\lnot p \land \lnot r) \op\equiv\hints{left part: extract common \;p \lor {}\;;}\hint{right part: extract common \;\lnot p \land {}\;} \big(p \lor (q \land q \land r)\big) \;\lor\; \big(\lnot p \land (\lnot q \lor \lnot r)\big) \op\equiv\hints{left part: simplify using idempotence of \;\land\;;}\hint{right part: simplify using DeMorgan} \big(p \lor (q \land r)\big) \;\lor\; \lnot \big(p \lor (q \land r)\big) \op\equiv\hint{excluded middle} \true \endcalc$$
So both sides of the original equivalence are $\;\true\;$, making the equivalence true as well.