⏎ back home

Making Sense of Proof by Contradiction

Table of contents

I’ve always felt uncertain about proof by contradiction. I’ve seen it done many times, and I know it is a valid approach, but I could never get myself to trust it.

I’ve been going through Goldrei’s Propositional and Predicate Calculus book these past few months. And while I’ve been lingering on chapter 2, some of the theorems and lemmas presented there finally made proof by contradiction click for me.

For what it is worth, I am no expert in any of this. It’s not only possible, but also extremely likely that something I say here is not accurate or has some of my misconceptions baked in.

What is proof by contradiction #

Suppose you have a set of axioms and assumptions Δ, and you want to prove that the statement φ is true when Δ is satisfied (i.e. Δ ⊨ φ). Proof by contradiction is one method you can use to establish that.

The approach is simple, but can be confusing due to all of the negations in my opinion.

To use proof by contradiction to show Δ ⊨ φ, you take a detour in your proof and see what happens when you assume that ¬φ is true alongside all of your other assumptions and axioms. During this detour, our goal is to show that from our original assumptions and axioms along with this new negated statement (i.e. { Δ ∪ ¬φ }) we can derive a contradiction.

What exactly does it mean to derive a contradiction?

If we can derive two statements ψ and ¬ψ from our set { Δ ∪ ¬φ }, then we have derived a contradiction. In other words, { Δ ∪ ¬φ } tells us that some statement ψ is true and false at the same time. A contradiction.

If we can show that a contradiction follows from { Δ ∪ ¬φ }, then we can pop all of these proof by contradictions off of our stack and declare with certainty that we have shown Δ ⊨ φ.

To say it all very concisely

Suppose you have a set of assumptions and axioms Δ and you wish to show Δ ⊨ φ

Show that { Δ ∪ ¬φ } ⊨ ψ and { Δ ∪ ¬φ } ⊨ ¬ψ

Now you know Δ ⊨ φ

What? #

Maybe this all feels really intuitive to someone somewhere out there… but to me, this has always felt a bit magical. I could never wrap my head around why we could intuit so much information from this alternate world where ¬φ is true.

On a certain level, I get the idea that the negation, the absence, or the negative space around something exactly describes the underlying thing… But I’ve never felt great about it, and I’ve never felt confident enough to lean into this reasoning in my own logic.

Relating Unsatisfiability and Logical Consequence #

Recently though, I learned how to reframe proof by contradiction as a statement about the unsatisfiability of sets of statements, and that helped a lot of things click into place for me. I’ll approach this by providing the theorems and proofs of the theorems, and then I’ll explain how these helped me understand proof by contradiction in the section below.

But before we can get into the theorems, we have to define satisfiability.

When we are considering some set of statements Γ, we can say that Γ is either satisfiable or unsatisfiable. If Γ is satisfiable, then there is some truth assignment under which every statement in Γ is true. If it is unsatisfiable, then there is no truth assignment that makes every statement in the set true.

With that established, let’s see the theorems:

Both of these theorems establish a relationship and equivalence between certain logical consequence statements and unsatisfiability. We’ll prove each of these in turn, but they both rely on a lemma that is useful to get out of the way first.

To prove this lemma, we consider the fact that every truth assignment must yield a true or false value for a particular formula. So, in the language of the lemma, for our truth assignment υ, φ must either evaluate to true or false, and ¬φ will evaluate to the opposite. And thus, υ satisfies exactly one of φ or ¬φ. (this proof is a bit hand-wavy, but I think a more complete proof would require more extensive definitions for truth assignments and statements than I want to get into in this post).

With the lemma settled, we move on to proving theorem 1. This theorem tells us that any statement of logical implication (Δ ⊨ φ) is equivalent to a statement about the unsatisfiability of the premises and the negated conclusion {Δ ∪ ¬φ}.

To prove this bi-conditional (“if and only if”) we need to show both directions of implication hold:

Direction 1: if {Δ ∪ ¬φ} is unsatisfiable then Δ ⊨ φ.

Direction 2: if Δ ⊨ φ then {Δ ∪ ¬φ} is unsatisfiable.

Now we can prove theorem 2. This theorem tells us that a set of statements deriving a contradiction (i.e. a formula φ and its negation ¬φ) is equivalent to the set of statements being unsatisfiable.

Direction 1: if there exists a statement φ such that Δ ⊨ φ and Δ ⊨ ¬φ then Δ is unsatisfiable.

Direction 2: if Δ is unsatisfiable there exists a statement φ such that Δ ⊨ φ and Δ ⊨ ¬φ.

Tying it all back to proof by contradiction #

Now let’s reframe proof by contradiction in terms of the theorems from above.

As we mentioned above, we use proof by contradiction as a means to show a particular logical consequence, like Δ ⊨ φ, holds.

And that’s it! That is proof by contradiction reframed in terms of some theorems that we can prove and understand.

In conclusion #

Seeing this all written out… I honestly don’t know that this understanding of proof by contradiction is any “simpler” per-se. But grounding the proof in theorems which we can prove went a long way towards making proof by contradiction feel less magical and more like a tool I can lean on moving forward.

There is a lot I feel that I am still missing or uncertain about though. My understanding of formal logic is currently limited to propositional logic, and so I am not sure how well this understanding will scale out as I learn more about first order logic and other logics.