Personal website

Proof

\begin{equation*} (P \implies Q) \> \not \equiv \> (Q \implies P). \end{equation*}

By the definition of the conditional and the biconditional,

\begin{align*} (P \implies Q) & \equiv (Q \implies P) \\ (\lnot P \lor Q) & \equiv (\lnot Q \lor P) \\ (\lnot P \lor Q) \implies (\lnot Q \lor P) \big) & \land \big( (\lnot Q \lor P) \implies (\lnot P \lor Q) \big) \\ \big( \lnot (\lnot P \lor Q) \lor (\lnot Q \lor P) \big) & \land \big( \lnot (\lnot Q \lor P) \lor (\lnot P \lor Q) \big), \end{align*}

which is not a tautology, as per

<<scheme/tautology?>>
(not (tautology? (lambda (p q)
                   (and (or (not (or (not p) q))
                            (or (not q) p))
                        (or (not (or (not q) p))
                            (or (not p) q))))
                 2))

#t

\(\blacksquare\)