Give an equational proof $ \vdash (p \lor \lnot r) \rightarrow (p \lor q) \equiv \lnot q \rightarrow (r \lor p)$

Question

Give an equational proof $$ \vdash (p \lor \lnot r) \rightarrow (p \lor q) \equiv \lnot q \rightarrow (r \lor p)$$

---

What I tried

$(p \lor \lnot r) \rightarrow (p \lor q)$

Applying De morgan

$\lnot(\lnot p \land r) \rightarrow (p \lor q)$

Applying Implication rule

$ (\lnot p \land r) \lor (p \lor q)$

Distributing

$[(p \lor q) \lor \lnot p] \land [(p \lor q) \lor r] $

And I couldn't continue.

See George Tourlakis, Mathematical Logic (2008) or this post for a list of axioms and theorems.

Answer 1

Picking up where you left off (the work you did is just fine)...

We can use associativity and commutativity of the $\lor$ connective on the first and second term:

$$\begin{align}[(p \lor q)\lor \lnot p] & \equiv p \lor q \lor \lnot p \tag{1}\\ \\ &\equiv p \lor \lnot p \lor q\\ \\ &\equiv (p \lor \lnot p) \lor q\\ \\ & \equiv T\lor q \\ \\ & \equiv T\end{align}$$

$$\begin{align} (p \lor q) \lor r & \equiv p\lor q \lor r \tag{2}\\ \\ &\equiv q \lor r \lor p \\ \\ &\equiv \lnot q\rightarrow (r\lor p)\end{align}$$

In the last step of $(2)$, we use the identity $a \lor b \equiv \lnot a \rightarrow b$.

Putting $(1)$ and (2) together gives us $$[(p \lor q)\lor \lnot p] \land [(p \lor q)\lor r ]\equiv T \land [\lnot q\rightarrow (r\lor p)] \equiv \lnot q \rightarrow (r \lor p)$$

Answer 2

Here is a shorter and more 'documented' proof, compared to the original answer to this old question.$ \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}{\top} \newcommand{\false}{\bot} $

Our strategy will be to start at the most complex side of the equivalence (the left hand side), simplify as much as possible, and then from that point work towards the other side.

So we calculate:

$$\calc p \lor \lnot r \;\then\; p \lor q \op\equiv\hints{expand $\;\then\;$ using theorem $(2.4.11)$ -- since $\;\then\;$ is usually more}\hint{difficult to manipulate, and this is the shortest way to expand it} \lnot (p \lor \lnot r) \lor p \lor q \op\equiv\hints{DeMorgan: theorem $(2.4.17)$; double negation: theorem $(2.4.4)$}\hint{-- this looks like the only way to make progress} (\lnot p \land r) \lor p \lor q \op\equiv\hints{distribute $\;{}\lor p\;$ over $\;\land\;$ by theorem $(2.4.23)(ii)$ and axiom $(6)$}\hint{-- to bring both $\;p\;$'s together in the hope of simplifying} ((\lnot p \lor p) \land (r \lor p)) \lor q \op\equiv\hint{excluded middle: axiom $(9)$ -- to simplify} (\true \land (r \lor p)) \lor q \op\equiv\hint{$\;\true\;$ is identity of $\;\land\;$, theorem $(2.4.20)$ -- to simplify some more} r \lor p \lor q \tag{*} \op\equiv\hints{reorder using symmetry of $\;\lor\;$, i.e., axiom $(6)$}\hint{-- working towards our goal} q \lor r \lor p \op\equiv\hint{reintroduce $\;\then\;$ using theorem $(2.4.11)$} \lnot q \;\then\; r \lor p \endcalc$$

which completes the proof.

Note how the steps up until $\Ref{*}$ were all more or less 'forced' by our strategy of simplifying, and from there the goal was directly within reach.

Also, note that his proof format implicitly uses transitivity $(1.4.13)(c)$ and Leibniz $(2.1.16)$. Also, I implicitly used associativity of $\;\lor\;$ $(5)$ by leaving out the parentheses in $\;A \lor B \lor C\;$, and occasionally symmetry of $\;\equiv\;$ $(2)$.