---
tags: logic, natural deduction, johanna
---

# Natural Deduction

Examples of natural deduction proofs that use proof by contradiction aka reductio ad absurdum (RAA). [^RAA] [^or-elim]

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

> $\neg B$
> ... (here we use some other assumptions we made)
> $B$ (now we have a contradiction between $\neg B$ and $B$)

$\neg\neg B$ (and we conclude $\neg\neg B$)

More generally,

> $A$ (assumption)
> ... (proof continues)
> $B\wedge\neg B$ (found a contradiction)

$\neg A$ (conclude the negation of $A$)

On the other hand,

> $\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 $\neg\neg B\vdash B$. (If one takes "liberal" RAA to include proofs such as the latter one, then one can derive double negation from RAA.)

[^or-elim]: We also use this form of or-elimination:

$A\vee B$
$\neg A$
$B$

(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\vdash 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), $\neg$ (not).
- A *proof* of $P\vdash 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](https://github.com/alexhkurz/programming-languages-2022/blob/main/resources/Gentzen-natural-deduction-rules.png) from Gentzens original paper for a summary of the rules.[^gentzen]
- 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](https://www.youtube.com/watch?v=dlUkeN7KqVA) look promising. [^RAAandIP]

[^RAAandIP]: 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.

[^gentzen]: Instead of $\&$ we write $\wedge$ for *and*, $\vee$ is *or*, the rules of the quantifiers $\forall$ for *for all* and $\exists$ for *there is* are not used in the following, instead of $\supset$ we write $\rightarrow$ for *implies* and the funny mountain symbol is Gentzen's notation for contradiction (or falsum or false), today mostly written as $\bot$.

## A Lemma (no reductio ad absurdum)

Implication $B\vdash A\to B$ [^implication2] [^relevance]

[^implication2]:

$B \vdash A\to B$

$B$
> $A$
> $B$ (copying the $B$, not needed)

$A\to B$

[^relevance]: 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](https://plato.stanford.edu/entries/logic-relevance/#ProThe), in which such proofs are not allowed.

## Warming Up

Double Negation $\neg\neg A\vdash A$ [^doublenegation]

[^doublenegation]:

$\neg\neg A\vdash A$

$\neg\neg A$
> $\neg A$
>
$A$

---

Ex Falso Quodlibet $A\wedge\neg A \vdash B$ [^exfalsoquodlibet]

[^exfalsoquodlibet]:
$A\wedge\neg A \vdash B$
$A\wedge\neg A$
> $\neg B$
> $A$
> $\neg A$
>
$\neg\neg B$
$B$

---

Implication $\neg A\vdash A\to B$ [^implication1]

[^implication1]:

$\neg A\vdash A\to B$

$\neg A$
> $A$
>> $\neg B$
>
> $B$

$A\to B$

---

Tertium Non Datur $\vdash A\vee\neg A$ [^tertiumnondatur]

[^tertiumnondatur]:

$\vdash A\vee\neg A$
> $\neg(A\vee\neg A)$
>
>> $A$
>> $A\vee\neg A$
>
> $\neg A$
> $A\vee\neg A$

$A\vee\neg A$

---

## Eliminating Negation

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

Negated Implication $\neg(A\to B)\vdash A\wedge\neg B$ [^negatedimplication]

[^negatedimplication]: $\neg(A\to B)\vdash A\wedge\neg B$ (uses Implication)

$\neg(A\to B)$
> $\neg A$
> $A\to B$
>
$\neg\neg A$
$A$
> $B$
> $A\to B$

$\neg B$

$A\wedge \neg B$

---

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

$A\wedge \neg B$
$A$
$\neg B$
> $A\to B$
> $B$

$\neg (A\to B)$

---

Negated Conjunction $\neg(A\wedge B)\vdash \neg A\vee\neg B$ [^negatedconjunction]

[^negatedconjunction]:
$\neg(A\wedge B)\vdash \neg A\vee\neg B$

$\neg(A\wedge B)$

> $\neg(\neg A\vee\neg B)$
>> $\neg A$
>> $\neg A\vee\neg B$
>>
> $A$
>> $\neg B$
>> $\neg A\vee\neg B$
>>
> $B$
> $A\wedge B$

$\neg A\vee\neg B$

---

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

$\neg A\vee\neg B$
> $A\wedge B$
> $A$
> $B$
> $\neg B$

$\neg(\neg A\vee\neg B)$

---

Negated Disjunction $\neg(A\vee B)\vdash \neg A\wedge\neg B$ [^negateddisjunction]

[^negateddisjunction]:

$\neg(A\vee B)\vdash \neg A\wedge\neg B$

$\neg(A\vee B)$
> $A$
> $A\vee B$
>
$\neg A$
> $B$
> $A\vee B$
>
$\neg B$

$\neg (A\wedge B)$

---

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

$\neg A\wedge\neg B$
$\neg A$
$\neg B$
> $A\vee B$
> $B$

$\neg(A\vee B)$

Implication again $A\to B\vdash \neg A\vee B$ [^implicationagain]

[^implicationagain]: $A\to B\vdash \neg A\vee B$ (uses Negated Disjunction and Double Negation)

$A\to B$

> $\neg(\neg A\vee B)$
> $\neg\neg A \wedge \neg B$
> $\neg\neg A$
> $\neg B$
> $A$
> $B$

$\neg A\vee B$

---

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

$\neg A\vee B$
> $A$
> $B$

$A\to B$

## More Training Questions

$\neg (P\to Q)\vee R\vdash Q\to R$

...

## Outlook

In many of the our proofs we used double negation, that is, $\neg\neg A\vdash 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 ...