In short. We start with an example: A ∧ B ⇒ C, C ⇒ D, … D ⇒ E, where B is an assumed condition and E is a contradictory condition. According to proof by contradiction, we conclude ¬B. We demonstrate the truth of this conclusion by proving B ⇒ C ∧ D ∧ … E and showing that this implication reduces to ¬B.

Background. When we construct proofs, we often use the technique of assuming something to be true while suspecting it is false and then proceeding to derive a contradiction which allows us to conclude (and prove) that what we assumed to be true is instead false.

I often wondered how the logic of this works. Maybe I learned it some long time ago, but I am not sure. As a matter of fact, I think I never learned it. Therefore, I thought it might be fun to do a bit of exploring in order to find out what the logic of proof by contradiction looks like, and this thread is the result.

Outline. Section A shows an example of the use of proof by contradiction, and section B reveals the logic behind the results in section A.

Proven statements are identified by numbers within parentheses.

A. An example of the use of proof by contradiction.

I guess there are many ways a proof by contradiction can go. I have chosen to demonstrate one of them.

1. First we start with a result we have proved, the statement or condition A:

A (1)

2. Then we assume B to be true. We deduce something from A and B:

A ∧ B ⇒ C (2)

3. Then we deduce something from C:

C ⇒ D (3)

4. Then another deducing step:

D ⇒ E (4)

where E is the contradictory condition we are seeking. We conclude from this:

¬B (5)

B. An analysis of the proof by contradiction in section A.

From the combined implications in section A, we here produce what we might call the grand formula of proof by contradiction. Then we proceed by showing that this formula reduces to (5).

1. First we use (1) in (2). Note: I use = instead of ⇔ since either means the same on Bool.

A ∧ B ⇒ C =

true ∧ B ⇒ C =

B ⇒ C (6)

2. Next we combine (6) and (3) into one condition:

(B ⇒ C) ∧ (C ⇒ D) (7)

We manipulate (7) by using (3) and A ⇒ B ≡ ¬A ∨ B:

(B ⇒ C) ∧ (C ⇒ D) =

(¬B ∨ C) ∧ (C ⇒ D) =

¬B ∧ (C ⇒ D) ∨ C ∧ (C ⇒ D) =

¬B ∧ (true) ∨ C ∧ (¬C ∨ D) =

¬B ∨ (C ∧ ¬C ∨ C ∧ D) =

¬B ∨ (false ∨ C ∧ D) =

¬B ∨ C ∧ D =

B ⇒ C ∧ D (8)

Let us compare (8) and (7) to see what these deductions have accomplished.

C ⇒ D in (7) has the effect on B ⇒ C in (7) that "∧ D" has been appended to B ⇒ C as B ⇒ C appears in (8). Also, it looks as if "C) ∧ (C ⇒" in (7) has been replaced by "C ∧" in (8).

3. Now we combine (8) and (4):

(B ⇒ C ∧ D) ∧ (D ⇒ E) (9)

By using (4), we treat (9) in the same way as we did (7). Essentially, the only difference between (9) and (7) is that in (9) B implies a double condition, C ∧ D, while in (7) a single condition, C. This complication proves to pose no problem though:

(B ⇒ C ∧ D) ∧ (D ⇒ E) =

(¬B ∨ C ∧ D) ∧ (D ⇒ E) =

¬B ∧ (D ⇒ E) ∨ C ∧ D ∧ (D ⇒ E) =

¬B ∧ (true) ∨ C ∧ D ∧ (¬D ∨ E) =

¬B ∨ (C ∧ D ∧ ¬D ∨ C ∧ D ∧ E) =

¬B ∨ (false ∨ C ∧ D ∧ E) =

¬B ∨ C ∧ D ∧ E =

B ⇒ C ∧ D ∧ E (10)

(10) is an example of what I call the grand formula of proof by contradiction.

4. Now I would like to study the contradictory condition E a bit closer so as to make the inconsistency evident, i.e. by producing "false". In practice, we don't usually do this, and we didn't in section A either. Assume that E has the form:

E ≡ E1 ∧ E2 (11)

where E1 and E2 contradict each other. Assume that we have proved:

E1 ⇒ ¬E2 (12)

Here, the inconsistency is clear since E2 in (11) and ¬E2 in (12) contradict each other per definition.

Now let us continue in order to produce "false". We manipulate the right hand side of (11) by using (12):

E1 ∧ E2 =

E1 ∧ E2 ∧ true =

E1 ∧ E2 ∧ (E1 ⇒ ¬E2) =

E1 ∧ E2 ∧ (¬E1 ∨ ¬E2) =

(E1 ∧ E2 ∧ ¬E1 ∨ E1 ∧ E2 ∧ ¬E2) =

(false ∨ false) =

false

We use this to substitute "false" for E1 ∧ E2 in (11) and get:

E = false (13)

5. Now we use (13) to substitute "false" for E in (10):

B ⇒ C ∧ D ∧ E =

B ⇒ C ∧ D ∧ false =

B ⇒ false =

¬B ∨ false =

¬B

which is the same as (5), and this finishes our analysis.