3

In forall x: Calgary, by P. D. Magnus, section 16.6 p. 153, appears this natural deduction proof using Fitch-style:

enter image description here

Shouldn't line 8 be Indirect Proof because he is not introducing a negation ?

F. Zer
  • 2,325
  • 1
  • 8
  • 21
  • 2
    It is introducing negation, particularly, $\lnot \lnot(A\lor \lnot A) \equiv (A\lor \lnot A)$, albeit, the text doesn't list these two steps, the first being $\lnot$ I, the second being DN (double negation). – amWhy Mar 03 '20 at 13:54
  • @Mauro ALLEGRANZA Thank you, it is on p. 153. – F. Zer Mar 03 '20 at 14:05
  • 2
    Ok, I was browsing a different version :-) In my "Calgary" page 153 is the first page of FOL... Having said that, based on the Appendix Basic deduction rules for TFL (end of the book), you are still right: the rule "if from $\lnot \mathcal A$ we have derived $\bot$, conclude with $\mathcal A$" is called Indirect proof. – Mauro ALLEGRANZA Mar 03 '20 at 14:09

1 Answers1

2

You are right, according to their definitions, it should be IP. In the development of the proof on the pages before, it actually does have $IP$ instead of $\neg I$ in the last line, so the $IP$ label in the finished proof is likely a typo.

That being said, one can define $IP$ in terms of $\neg I$, but with an additional step, double negation elimination ($DNE$): 

m   | | ¬A
    | |---
    | | ...
n   | | ⊥
n+1 | ¬¬A    (¬I, m-n)
n+2 | A      (DNE, n+1)

where $DNE$ means going from $\neg \neg A$ to $A$.

But since $DNE$ is an additional (implicit) inference step that isn't valid in all logics that have $\neg I$ (namely in intuitionistic logic), one shouldn't conflate $IP$ with $\neg I$, and they don't do so in their rule definitions -- so this an inconsistency, and probably an error.

Natalie Clarius
  • 10,530