1
$\begingroup$

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}$.

$\endgroup$
  • 1
    $\begingroup$ Use a truth table $\endgroup$ – Ariana Aug 10 '16 at 4:11
  • $\begingroup$ I believe you mean to prove it using natural deduction? That's a legitimate question. It also leaves open the question of whether it can be proven without using the introduction rule of the excluded middle. $\endgroup$ – DanielV Aug 10 '16 at 4:15
  • $\begingroup$ what is " orElim and ⊥Intro"? $\endgroup$ – davyjones Aug 10 '16 at 4:18
  • 1
    $\begingroup$ @davyjones Or-Elimination is the inference rule that says "from $a \lor b,~a\implies c,~b\implies c$ infer $c$" . $\bot$-intro is probably "from $A \land \lnot A$ infer $\bot$", a rule which is actually redundant if you otherwise define $\lnot A$ to mean $A \implies \bot$. $\endgroup$ – DanielV Aug 10 '16 at 4:21
  • $\begingroup$ Establishing $p \land \lnot q \vdash \lnot (p \implies q)$ is rather easy, I suggest starting with that one. Unfortunately, I don't know kripke frames well enough to whether the other direction is derivable without excluded middle. $\endgroup$ – DanielV Aug 10 '16 at 4:25
2
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

$\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$)

$\endgroup$
0
$\begingroup$

$$\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}$$

$\endgroup$
  • $\begingroup$ See my answer for a direct proof without going through LEM, as well as an explanation of why it is not provable without DNE (or its consequent LEM), namely that it is intuitionistically invalid. I learned this nice thing from the linked post just a few months ago. =) $\endgroup$ – user21820 Aug 13 '16 at 8:28
  • $\begingroup$ @user21820 Your proof is much more direct than mine. I should have taken some time to determine if $\lnot (p \implies q) \implies (p \land \lnot q) \vdash \text{L.E.M.}$, that would be enough to determine that it is necessary. Your proof does use LEM though, just disguised as DNE. $\endgroup$ – DanielV Aug 13 '16 at 11:20
  • $\begingroup$ Indeed my last paragraph is equivalent to what you're saying, since we get DNE from the given equivalence. And yes there's no difference between DNE and LEM over the rest of classical logic, so it's a matter of aesthetic preference to pick one over the other. I guess some pick DNE because it involves only one connective. $\endgroup$ – user21820 Aug 13 '16 at 11:31
  • $\begingroup$ But from a classical logic perspective LEM is the natural version, and I do consider LEM to be fundamental (see math.stackexchange.com/a/1668149), and DNE to be the natural consequence of LEM. $\endgroup$ – user21820 Aug 13 '16 at 11:38
-1
$\begingroup$

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.

enter image description here

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/

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.