Natural Deduction

Examples of natural deduction proofs that use proof by contradiction aka reductio ad absurdum (RAA). ^{[1] [2]}

(All of the statements can be easily verified using truth tables. It is instructive to compare the method of truth tables with the natural deduction proofs.)

Remark on Notation: If

$P$ and

$Q$ are logical formulas, then

$P⊢Q$ claims that there is a proof of

$Q$ assuming

$P$. Below, the task is to find such proofs. For this to make sense, we need to agree on what is meant by formula and by proof.

• A formula is built from "atomic propositions" denoted
  $A,B$, etc and logical operations
  $\wedge$ (and),
  $\vee$ (or),
  $\to$ (implies),
  $\mathrm{\neg }$ (not).
• A proof of
  $P⊢Q$ is a sequence of formulas (each written in their own line), starting with the assumption
  $P$ and finishing with the conclusion
  $Q$. Each line needs to be justified by a rule and the formulas appearing before. The rules are Gentzen's rules of natural deduction. See this screenshot from Gentzens original paper for a summary of the rules.^[3]
• The Fitch style method of writing proofs I employ in the following uses indentation in the same way as it is used in programming languages such as Python, see eg https://plato.stanford.edu/entries/natural-deduction/#ModeVersJaskMeth . (Each time one makes a new assumption, one increases indentation; each time one introduces an implication
  $A\to B$ the assumption is "cancelled" by decreasing the level of indentation.)
• For more details, these videos look promising. ^[4]

A Lemma (no reductio ad absurdum)

Implication

$B⊢A\to B$ ^{[5] [6]}

Warming Up

Double Negation

$\mathrm{\neg }\mathrm{\neg }A⊢A$ ^[7]

Ex Falso Quodlibet

$A\wedge \mathrm{\neg }A⊢B$ ^[8]

Implication

$\mathrm{\neg }A⊢A\to B$ ^[9]

Tertium Non Datur

$⊢A\vee \mathrm{\neg }A$ ^[10]

Eliminating Negation

Also show the directions from right to left (which are easier).

Negated Implication

$\mathrm{\neg }(A\to B)⊢A\wedge \mathrm{\neg }B$ ^[11]

Negated Conjunction

$\mathrm{\neg }(A\wedge B)⊢\mathrm{\neg }A\vee \mathrm{\neg }B$ ^[12]

Negated Disjunction

$\mathrm{\neg }(A\vee B)⊢\mathrm{\neg }A\wedge \mathrm{\neg }B$ ^[13]

Implication again

$A\to B⊢\mathrm{\neg }A\vee B$ ^[14]

More Training Questions

$\mathrm{\neg }(P\to Q)\vee R⊢Q\to R$

…

Quantifiers

…

Outlook

In many of the our proofs we used double negation, that is,

$\mathrm{\neg }\mathrm{\neg }A⊢A$. These proofs are also known as proofs by contradiction or indirect proofs.

The logic in which one removes double negation is called intuitionistic logic.

It is interesting to think about whether it is possible to replace our proofs by contradiction with constructive proofs, that is, proofs that do not use double negation, that is, proofs in intuitionistic logic.

The answer is no, but for this we would need to find an interpretation of intuitionistic logic that provides a counter example of double negation.

Maybe more on this later …

---

1. The following are not "proper" RAA, but just negation-introduction (ie the proof of a negated statement):

   $\mathrm{\neg }B$
   … (here we use some other assumptions we made)
   

   $B$ (now we have a contradiction between

   $\mathrm{\neg }B$ and

   $B$)

   $\mathrm{\neg }\mathrm{\neg }B$ (and we conclude
   $\mathrm{\neg }\mathrm{\neg }B$)

   More generally,

   $A$ (assumption)
   … (proof continues)
   

   $B\wedge \mathrm{\neg }B$ (found a contradiction)

   $\mathrm{\neg }A$ (conclude the negation of
   $A$)

   On the other hand,

   $\mathrm{\neg }B$
   …
   contradiction

   $B$

   is a "proper" RAA proof. As one can see, in the latter case one additionally uses the principle of double negation, that is

   $\mathrm{\neg }\mathrm{\neg }B⊢B$. (If one takes "liberal" RAA to include proofs such as the latter one, then one can derive double negation from RAA.) ↩︎

2. We also use this form of or-elimination:

   $A\vee B$
   
   $\mathrm{\neg }A$
   
   $B$ ↩︎

3. Instead of

   $\mathrm{\&}$ we write
   $\wedge$ for and,
   $\vee$ is or, the rules of the quantifiers
   $\mathrm{\forall }$ for for all and
   $\mathrm{\exists }$ for there is are not used in the following, instead of
   $\supset$ we write
   $\to$ for implies and the funny mountain symbol is Gentzen's notation for contradiction (or falsum or false), today mostly written as
   $\mathrm{\perp }$. ↩︎

4. The video calls RAA what I call negation introduction and calls indirect proof what I call proper RAA and do in two steps via negation introduction and double negation elimination. ↩︎

5. $B⊢A\to B$
   $B$

   $A$
   

   $B$ (copying the

   $B$, not needed)

   $A\to B$ ↩︎

6. The proof is strange in that the conclusion

   $B$ does not depend on
   $A$. (Or, in other words, if we do not allow copying, the conclusion
   $B$ comes before the assumption
   $A$ in the deduction.) There is a logic, relevance logic, in which such proofs are not allowed. ↩︎

7. $\mathrm{\neg }\mathrm{\neg }A⊢A$
   $\mathrm{\neg }\mathrm{\neg }A$

   $\mathrm{\neg }A$

   $A$

   ---

   ↩︎

8. $A\wedge \mathrm{\neg }A⊢B$
   
   $A\wedge \mathrm{\neg }A$

   $\mathrm{\neg }B$
   

   $A$
   

   $\mathrm{\neg }A$

   $\mathrm{\neg }\mathrm{\neg }B$
   
   $B$

   ---

   ↩︎

9. $\mathrm{\neg }A⊢A\to B$
   $\mathrm{\neg }A$

   $A$

   $\mathrm{\neg }B$

   $B$

   $A\to B$

   ---

   ↩︎

10. $⊢A\vee \mathrm{\neg }A$

    $\mathrm{\neg }(A\vee \mathrm{\neg }A)$

    $A$
    

    $A\vee \mathrm{\neg }A$

    $\mathrm{\neg }A$
    

    $A\vee \mathrm{\neg }A$

    $A\vee \mathrm{\neg }A$

    ---

    ↩︎

11. $\mathrm{\neg }(A\to B)⊢A\wedge \mathrm{\neg }B$ (uses Implication)
    $\mathrm{\neg }(A\to B)$

    $\mathrm{\neg }A$
    

    $A\to B$

    $\mathrm{\neg }\mathrm{\neg }A$
    
    $A$

    $B$
    

    $A\to B$

    $\mathrm{\neg }B$
    $A\wedge \mathrm{\neg }B$

    ---

    The other direction does not use double negation (proper RAA):

    $A\wedge \mathrm{\neg }B$
    
    $A$
    
    $\mathrm{\neg }B$

    $A\to B$
    

    $B$

    $\mathrm{\neg }(A\to B)$

    ---

    ↩︎

12. $\mathrm{\neg }(A\wedge B)⊢\mathrm{\neg }A\vee \mathrm{\neg }B$
    $\mathrm{\neg }(A\wedge B)$

    $\mathrm{\neg }(\mathrm{\neg }A\vee \mathrm{\neg }B)$

    $\mathrm{\neg }A$
    

    $\mathrm{\neg }A\vee \mathrm{\neg }B$

    $A$

    $\mathrm{\neg }B$
    

    $\mathrm{\neg }A\vee \mathrm{\neg }B$

    $B$
    

    $A\wedge B$

    $\mathrm{\neg }A\vee \mathrm{\neg }B$

    ---

    The other direction does not use double negation (proper RAA):

    $\mathrm{\neg }A\vee \mathrm{\neg }B$

    $A\wedge B$
    

    $A$
    

    $B$
    

    $\mathrm{\neg }B$

    $\mathrm{\neg }(\mathrm{\neg }A\vee \mathrm{\neg }B)$

    ---

    ↩︎

13. $\mathrm{\neg }(A\vee B)⊢\mathrm{\neg }A\wedge \mathrm{\neg }B$
    $\mathrm{\neg }(A\vee B)$

    $A$
    

    $A\vee B$

    $\mathrm{\neg }A$

    $B$
    

    $A\vee B$

    $\mathrm{\neg }B$
    $\mathrm{\neg }(A\wedge B)$

    ---

    The other direction does not use double negation (proper RAA):

    $\mathrm{\neg }A\wedge \mathrm{\neg }B$
    
    $\mathrm{\neg }A$
    
    $\mathrm{\neg }B$

    $A\vee B$
    

    $B$

    $\mathrm{\neg }(A\vee B)$ ↩︎

14. $A\to B⊢\mathrm{\neg }A\vee B$ (uses Negated Disjunction and Double Negation)
    $A\to B$

    $\mathrm{\neg }(\mathrm{\neg }A\vee B)$
    

    $\mathrm{\neg }\mathrm{\neg }A\wedge \mathrm{\neg }B$
    

    $\mathrm{\neg }\mathrm{\neg }A$
    

    $\mathrm{\neg }B$
    

    $A$
    

    $B$

    $\mathrm{\neg }A\vee B$

    ---

    The other direction does not use double negation (proper RAA):

    $\mathrm{\neg }A\vee B$

    $A$
    

    $B$

    $A\to B$ ↩︎