I'm reading through an introduction to logic textbook and cannot follow an example on natural deduction rules.

I couldn't find a way to nicely typeset the deduction tree in MathJax, so I'll instead name each deduction with a roman numeral and build the tree by referencing those names; please do advise me on a better method if you know one. I'll use $I$ for introduction and $E$ for elimination.

The example follows:

Prove: $\vdash \neg(A \implies B) \implies A$

  • $(i) \frac{[A]^1 \quad [\neg A]^2}{A \land \neg A}, \land I$
  • $(ii) \frac{(i)}{\neg \neg B}, \neg I$
  • $(iii) \frac{(ii)}{B}, \neg E$
  • $(iv) \frac{(iii)}{A \implies B}, \Rightarrow I, 1$
  • $(v) \frac{(iv) \quad [\neg(A \implies B)]^3}{(A \implies B) \land \neg(A \implies B)}, \land I$
  • $(vi) \frac{(v)}{\neg \neg A}, \neg I, 2$
  • $(vii) \frac{(vi)}{A}, \neg E$
  • $(viii) \frac{(vii)}{\neg (A \implies B) \implies A}, \Rightarrow I, 3$

The example has a verbal explanation that I'll translate from the original Finnish:

The thought process behind this somewhat convoluted reasoning is as follows. We assume $\neg (A \implies B)$. If $\neg A$ then from $A$ through the contradiction $A \land \neg A$ we can deduce $B$, i.e. we get $A \implies B$. This contradicts the assumption $\neg (A \implies B)$. Therefore the assumption $\neg A$ lead to a contraction and we can deduce that $A$ must be true.

I do not understand the reasoning behind step (ii). Since (a) we deduce $\neg\neg B$ instead of $B$ and (b) the book doesn't introduce the "ex contradictione quodlibet" rule until much later, I assume it's not by the principle of explosion that we get (ii). The text starts by assuming $\neg (A \implies B)$ which is clearly equivalent to $A \land \neg B$; is that's what's being used here? If so, I don't see how it's used in (ii).

Edit: The book defines the rules for the introduction and elimination of negation as: $$\frac{\neg\neg A}{A}, \neg E \quad \frac{\substack{[B] \\ \vdots \\ A \land \neg A}}{\neg B}, \neg I$$

I understand the introduction rule to mean "if we can deduce $A \land \neg A$ (a contradiction) from $B$ being true, then we know that $B$ must not be true." In this problem, I do not see how we deduce $A \land \neg A$ from $\neg B$: I do not see how $B$ can influence steps (i) and (ii) at all, at least in the problem as it is described.

I'd love to have a clearer more "dumbed down" explanation of the whole deduction process but would also appreciate any pointers to what happens in (ii)

The original Finnish text:

Tämän hieman mutkikkaan päättelyn ajatuskulku on seuraava. Oletetaan, että $\neg (A \implies B)$. Jos $\neg A$, niin lauseesta $A$ voidaan ristiriidan $A \land \neg A$ kautta päätellä $B$, eli saadaan $A \implies B$. Tämä on ristiriidassa oletuksen $\neg (A \implies B)$ kanssa. Siis oletus $\neg A$ johti ristiriitaan ja voimme päätellä, että $A$ pätee.

Source of the problem:
Example 55 of Johdatus logiikkaan, H. Salminen & J. Väänänen 1992, 7th edition (2005), Oy Yliopistokustannus University Press Finland, ISBN: 951-662-549-5

  • 1
    $\begingroup$ Welcome to Math.SE! I believe you can use \cfrac inside a double-dollar-sign environment to typeset deduction trees here, but what you did is actually much easier to read on smartphones and small screens, so you should stick with it for now. $\endgroup$
    – Z. A. K.
    Commented Jun 22 at 17:17
  • 2
    $\begingroup$ I am not sure what rules are used in this specific textbook: natural deduction is not standardized across books, and has various different presentations. Can you explain how your $\neg I$ rule works? Does it let you introduce $\neg X$ for any $X$ using a contradiction as a premise? Does $\neg T$ let you introduce $\neg Y$ while discharging some hypothesis $Y$? If so, then you get (ii) simply by choosing $X$ as $\neg B$ in $\neg I$! And alternatively could also have obtained it by additionally assuming $[\neg B]_4$ in (i) then immediately discharging it via $\neg T,4$ instead. $\endgroup$
    – Z. A. K.
    Commented Jun 22 at 17:30
  • $\begingroup$ Thank you @Z.A.K.! That's a good point about the rules not being standard across textbooks, I'll amend my question with the introduction and elimination rules for negation in this particular book. I accidentally let the book-original $\neg T$ slip in (vi) instead of the intended $\neg I$; did you reference that typo with $\neg T$ in your comment or does $\neg T$ mean something else there? $\endgroup$
    – Emma
    Commented Jun 22 at 17:41
  • 1
    $\begingroup$ Step (i) had two assumptions, $A$ and $\neg A$, but it can be viewed as also having a third assumption, namely $\neg B$, that just happens not to be used. Now you can apply $\neg I$ to deduce $\neg\neg B$ while discharging the assumption $\neg B$. If you insist that assumptions must be used, then just insert into the proof some irrelevant lines that use $\neg B$; for example, from $\neg B$ and $A$ infer $A\land\neg B$, and from that infer $A$. $\endgroup$ Commented Jun 22 at 19:59
  • $\begingroup$ Hmmh, I still have trouble really understanding what's happening here — probably because I'm a novice in the field. If I assume $A$ and $\neg A$ and $\neg B$, I simply don't see how we reason the contradiction of $A$ and $\neg A$ from $B$, which I understood to be the prerequisite for the "proof by contradiction" that's required for $\neg I$. Currently, only if I know that e.g. $\neg B \equiv A \land \neg A$ can I see that it must follow that $\neg B$ must not be true, i.e. $\neg\neg B$. It's difficult to explain what I don't understand but hopefully that illustrates where I'm stuck. $\endgroup$
    – Emma
    Commented Jun 22 at 20:24

1 Answer 1


Let's put it together in one diagram. $${viii}\dfrac{\hspace{-3ex}{vii}\dfrac{\hspace{-2.5ex}{vi}\dfrac{\hspace{-2ex}{v}\dfrac{\hspace{-2ex}{iv}\dfrac{\hspace{-3ex}{iii}\dfrac{\hspace{-2ex}{ii}\dfrac{\hspace{-1.5ex}{i}\dfrac{[A]^1\quad[\neg A]^2}{A\land\neg A}{\land\mathrm I}\hspace{-3ex}}{\neg\neg B}{\neg\mathrm I}\hspace{-3ex}}{B}{\neg\mathsf E}\hspace{-3ex}}{A\to B}{{\to}\mathrm I^1}\quad\lower{1ex}{[\neg(A\to B)]^3}}{(A\to B)\land\neg(A\to B)}{\land\mathrm I}\hspace{-3ex}}{\neg\neg A}{\neg\mathrm I^2}\hspace{-4ex}}{A}{\neg\mathrm E}\hspace{-4ex}}{\neg(A\to B)\to A}{{\to}\mathrm I^3}$$

I do not understand the reasoning behind step (ii). Since (a) we deduce ¬¬B instead of B and (b) the book doesn't introduce the "ex contradictione quodlibet" rule until much later, I assume it's not by the principle of explosion that we get (ii).

No; it is written right there: They used negation introduction. Which is:

$\quad\neg\mathrm I$ : When you have derived a contradiction under an assumption, you may discharge occurrences of that assumption (including no occurrence) to deduce its negation.

They could have made the assumption then immediately discharged it: $\dfrac{\dfrac{A\quad \neg A}{A\land\neg A}\quad\lower{2ex}{[\neg B]^0}}{\neg\neg B}{\neg\mathrm I^0}$ . However, what they did do is legitimate.

Remember: if you can derive a thing from some assumptions, you can also derive it from those assumptions plus additional assumptions.

You cannot immediately deduce the proposition $B$ using negation introduction, because there is no negation in $B$ to introduce (so what assumption could you discharge?).

However, having derived $\neg\neg B$ they then use their rule of $\neg\mathrm E$ to eliminated the double negation (this rule is more often known as $\neg\neg\mathrm E$).

Once you are taught the rule of ex quod libet (explosion), it basically combines those two steps. But as you say, it had not been taught at this point.

The text starts by assuming $¬(A⟹B)$ which is clearly equivalent to $A∧¬B$ ; is that's what's being used here? If so, I don't see how it's used in (ii).

That is because it is not used in stage (ii). It is used in stage (v), and discharged in stage (viii). Hence the superscript : ${\to}\mathrm I^3$ discharges $[\neg(A\to B)]^3$ and the derived $A$, deduce: $\neg(A\to B)\to A$.

Here's a Fitch style version of that proof:

$$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \fitch{}{\fitch{~~1.~~\neg(A\to B)}{\fitch{~~2.~~\neg A}{\fitch{~~3.~~A}{~~4.~~A\land\neg A\hspace{18.5ex}{\land}\mathrm I~2,3\\~~5.~~\neg\neg B\hspace{21ex}{\neg}\mathrm I~(\neg B){-}4\\~~6.~~B\hspace{24ex}\neg\neg\mathrm E~5}\\~~7.~~A\to B\hspace{22ex}{\to}\mathrm I~3{-}6\\~~8.~~(A\to B)\land\neg(A\to B)\hspace{7ex}{\land}\mathrm I~7,1}\\~~9.~~\neg\neg A\hspace{27.5ex}\neg\mathrm I~2{-}8\\10.~~A\hspace{30.5ex}\neg\neg\mathrm E~9}\\11.~~\neg(A\to B)\to A\hspace{20ex}{\to}\mathrm I~1{-}10}$$

  • $\begingroup$ Thank you! I think this gets me closer to what I'm struggling with. What the application of $\neg I$ looks like to me here is something like this. Say we have $A \equiv 1 = 1$. We assume $A$ and simultaneously $\neg A$. We then have e.g. $B \equiv \text{'dogs are cute'}$ and we assume $\neg B$. Now we say with $\neg I$ that from these assumptions it must follow that dogs are cute. Which (while being a true statement if you ask me) is an absurd line of reasoning, not least because the variables at play (the identity of $1$ and the cuteness of dogs) have nothing to do with each other. $\endgroup$
    – Emma
    Commented Jun 23 at 9:41
  • 1
    $\begingroup$ We call it a vacuously valid argument: an argument which is valid because the premises are absurd. An argument is valid when there is no interpretation where the conclusion is false and the premises all true. But a contradiction is never true, so...$$\text{$A$ and $\neg A$ entail $\neg\neg B$}$$ $\endgroup$ Commented Jun 24 at 3:24
  • $\begingroup$ Alright, I'm satisfied this answers my original question and I'll mark it as solved. Thank you very much for your time! I still don't really intuitively see how this holds water but there's a lot of searchable keywords here to start digging. $\endgroup$
    – Emma
    Commented Jun 24 at 14:03

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .