Prove that $\lnot (p \implies q)$ is equivalent to $p \land \lnot q$?

Question

By equivalent I mean the biconditional, as in $$\lnot (p \implies q) \iff p \land \lnot q$$

Given the definition of implication, I understand why this is true, but I need a bit of help showing this with a formal proof using rules like $\lor-\text{Elim}$ and $\bot-\text{Intro}$.

Answer 1

Here is the pure natural deduction proof (Fitch-Style).

---

If $p \land \neg q$:

  $p$;

  $\neg q$.

  If $p \to q$:

    ...

    $\bot$.

  $\neg( p \to q )$.

If $\neg( p \to q )$:

  If $\neg p$:

    If $p$:

      $\bot$.

      $q$.

    $p \to q$.

    $\bot$.

  $\neg \neg p$.

  $p$.

  If $q$:

    ...

    $p \to q$.

    $\bot$.

  $\neg q$.

  $p \land \neg q$.

$p \land \neg q \leftrightarrow \neg( p \to q )$.

---

I'll leave you to fill in the blanks, which should be easy. See this post for a brief description of the general method to discovering such a proof. Sometimes it can be convenient to use LEM (law of excluded middle) to split cases in a clever manner to shorten the proof, but that way requires some experience.

As for the interesting side question of whether or not one can prove the equivalence in intuitionistic logic, which has the same inference rules except without DNE (double negation elimination), and hence LEM does not hold, the answer is that indeed it cannot be done. Note that the above proof only uses DNE once. Feel free to ignore the rest of this post if you are not interested in intuitionistic logic.

In intuitionistic logic, "$\neg p$" is simply a short-form for "$p \to \bot$". To prove that some sentence is not provable in intuitionistic logic, it suffices to construct a Kripke frame that does not satisfy it (see this post). Consider the Kripke frame $0 \to 1$ where $p$ is known only at $1$ and $q$ is not known at both $0,1$. Then $\neg( p \to q )$, which denotes $( p \to q ) \to \bot$, is known everywhere, but $p \land \neg q$ is not known at $0$.

Alternatively, note that if it were provable in intuitionistic logic, it would hold when $q = \bot$, but that gives $\neg( p \to \bot ) \to p \land ( \neg \bot )$, which is equivalent (by definition) to $\neg \neg p \to p$, which is not valid in intuitionistic logic.

Answer 2

$\lnot (p \implies q) \equiv \lnot (q \lor \lnot p)$ (definition of implication)

$\lnot (q \lor \lnot p)\equiv (\lnot q)\land \lnot(\lnot p)$ (de Morgan's law)

$(\lnot q)\land \lnot(\lnot p)\equiv \lnot q\land p$ (involution of $\lnot$)

$\lnot q\land p \equiv p\land \lnot q$ (commutativity of $\land$)

Answer 3

$$\newcommand{\DeductionBox} [1]{\begin{array} {l|} #1 \\ \hline \end{array}}$$

The reverse direction is straightforward:

$$\begin{array} {l} \begin{array} {rlr} (1) & p \land \lnot q & \text{Given} \\ (2) & p & \land\text{-Elimination of }(1) \\ (3) & \lnot q & \land\text{-Elimination of }(1) \\ \end{array}\\ \\ \DeductionBox{ \begin{array} {rlr} \quad (4) & p \implies q & \text{New Assumption} \\ \quad (5) & q & \implies\text{-Elimination of }(4) \text{ and } (2) \\ \quad (6) & \bot & \bot\text{-Introduction of }(5) \text{ and }(3) \end{array} \\ } \\ \\ \begin{array} {rlr} (7) & (p \implies q) \implies \bot & \quad\implies-\text{Introduction of }(4) \text{ to } (6) \\ (8) & \lnot (p \implies q) & \lnot-\text{Introduction of }(7) \\ \end{array} \end{array}$$

$$~$$ $$~$$ The foward direction can be done using the law of the excluded middle:

$$\begin{array} {l} \begin{array} {rlr} (1) & \lnot (p \implies q) & \text{Given} \\ (2) & \bot \implies \lnot q & \text{Vaccous Implication } \\ \end{array}\\ \\ \DeductionBox{ \begin{array} {rlr} \quad (3) & p & \text{New Assumption} \\ \end{array} \\ \\ \DeductionBox{ \begin{array} {rlr} \quad \quad (4) & q & \text{New Assumption} \\ \end{array} \\ \\ \DeductionBox{ \begin{array} {rlr} \quad \quad \quad (5) & p & \text{New Assumption} \\ \quad \quad \quad (6) & q & \text{Copy of }(4) \\ \end{array} \\ }\\ \\ \begin{array} {rlr} \quad \quad (7) & p \implies q & \implies\text{-Introduction of }(5) \text{ to }(6) \\ \quad \quad (8) & \bot & \bot\text{-Introduction of }(7) \text{ and }(1) \\ \quad \quad (9) & \lnot q & \implies\text{-Elimination of }(2) \text{ and }(8) \\ \quad \quad (10) & p \land \lnot q & \land\text{-Introduction of }(3) \text{ and }(9) \\ \end{array} \\ }\\ \\ \DeductionBox{ \begin{array} {rlr} \quad \quad (11) & \lnot q & \text{New Assumption} \\ \quad \quad (12) & p \land \lnot q & \land\text{-Introduction of }(3)\text{ and }(11) \\ \end{array} \\ }\\ \\ \begin{array} {rlr} \quad (13) & q \implies (p \land \lnot q) & \implies\text{-Elimination of }(4)\text{ to }(10) \\ \quad (14) & \lnot q \implies (p \land \lnot q) & \implies\text{-Elimination of }(11)\text{ to }(12) \\ \quad (15) & q \lor \lnot q & \text{Law of the Excluded Middle} \\ \quad (16) & p \land \lnot q & \lor\text{-Elimination of }(15),(13),(14) \\ \end{array} \\ } \\ \\ \DeductionBox{ \begin{array} {rlr} \quad (17) & \lnot p & \text{New Assumption } \\ \end{array}\\ \\ \DeductionBox{ \begin{array} {rlr} \quad \quad (18) & p & \text{New Assumption} \\ \quad \quad (19) & \bot & \bot\text{-Introduction of }(18)\text{ and }(17) \\ \quad \quad (20) & \bot \implies q & \text{Vaccuous Implication} \\ \quad \quad (21) & q & \implies\text{-Elimination of }(20)\text{ and }(19) \\ \end{array} \\ }\\ \\ \begin{array} {rlr} \quad (22) & p \implies q & \implies\text{-Introduction of }(18)\text{ to }(21) \\ \quad (23) & \bot & \implies\text{-Elimination of }(1)\text{ and }(22) \\ \quad (24) & \lnot q & \implies\text{-Elimination of }(2)\text{ and }(23) \\ \quad (25) & p \land \lnot q & \land\text{-Introduction of }(3)\text{ and }(24) \\ \end{array}\\ }\\ \begin{array} {rlr} (26) & p \implies (p \land \lnot q) & \implies\text{-Elimination of }(3)\text{ to }(16) \\ (27) & \lnot p \implies (p \land \lnot q) & \implies\text{-Elimination of }(17)\text{ to }(25) \\ (28) & p \lor \lnot p & \text{Law of the Excluded Middle} \\ (29) & p \land \lnot q & \lor\text{-Elimination of }(28),(26),(27) \\ \end{array}\\ \end{array}$$

Answer 4

The OP is looking for the following:

Given the definition of implication, I understand why this is true, but I need a bit of help showing this with a formal proof using rules like ∨−Elim and ⊥−Intro.

The following proof uses disjunction elimination ("∨−Elim" or "vE") on line 20 and negation introduction ("⊥−Intro" or "⊥I") on lines 6 and 21.

For a description of the justification used see the text forallx and the associated proof checker referenced below.

---

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/