Proof by Contradiction vs. Proof of Negation

Question

In constructive mathematics we make a distinction between "proof of negation" and "proof by contradiction". You can read a great account of the difference in this blog post of Andrej Bauer.

To summarize

1. Proof of negation is proving $\neg p$ by assuming $p$ and arguing an absurdity.
2. Proof by contradiction is proving $p$ by assuming $\neg p$ and arguing an absurdity.

I am writing an introduction to proof book which puts Fitch style natural deduction introduction and elimination rules front and center. My definition of negation is $\neg p \equiv (p \implies \bot)$ where $\bot$ stands for an absurdity. The introduction rule for negation is thus the proof pattern we would call "proof of negation" above.

I am looking for a big list of elementary arguments which are actually proof by contradiction rather than proof of negation. I need these for the section of my textbook which covers the "proof by contradiction" strategy. It is exceedingly difficult to find elementary situations where proof by contradiction is actually an appropriate strategy.

Here is one example of each strategy:

Proof of negation

$6$ is not odd.

Assume that $6$ is odd. Then there is an integer $k$ with $6=2k+1$. Solving for $k$ yields $k=2.5$ which is not an integer. This is a contradiction. Thus $6$ is not odd.

Proof by contradiction

I steal an example from Neil Strickland: Some non-zero digit occurs infinitely often in the decimal expansion of $\pi$.

Proof: Assume to the contrary that every non-zero digit appears finitely many times in the decimal expansion of $\pi$. Then $\pi$ would be a rational number. However $\pi$ is known to be irrational. Contradiction.

In this argument we obtain a contradiction by assuming the negation of what we are trying to prove. Note that it does not actually produce an explicit example of a non-zero digit which occurs infinitely often (if it did the proof would be constructive).

UPDATE: I made the following table for my book. Perhaps it will inspire some more ideas. All of the current answers (I think) showcase the consequence of proving an existentially quantified statement by contradiction: that you cannot actually show me how to produce a witness. It would be interesting to see examples of proofs by contradiction which showcase the other sacrifices.

Type of statement	The sacrifice we make using proof by contradiction
$p \vee q$	I know that either $p$ or $q$ is true, but I cannot tell you which one.
$p \wedge q$	I don't have a direct argument for $p$ and $q$ independently.
$\neg p$	There is no sacrifice. $\neg p$ is equivalent to $\neg (\neg (\neg p))$ in intuitionist logic as well. A bit weird to do though.
$p \implies q$	If you hand me an argument that $p$ is true, I do not actually have a way to use that data to argue $q$. To argue that $q$ is true I would need to pay the associated cost with whatever kind of statement $q$ is.
$\exists x \in U: A(x)$	While I know that some $x_1 \in U$ makes $A(x_1)$ true, I do not know how to actually show you one.
$\forall x \in U: A(x)$	If you hand me a particular $x_1 \in U$ I don't have a direct argument that $A(x_1)$ is true. I can only show you that assuming it is not true leads to contradiction. In other words, whatever type of statement $A(x_1)$ is, I will pay the associated price for that statement.

Answer 1

I believe good examples for proofs by contradiction will be hard to come by. The reason is that a proof by contradiction of $\phi$ actually proves $\neg \neg \phi$, a statement without any ``constructive content'' whatsoever. Usually, our proofs will contain some actual constructive content (even if not enough to be entirely constructive), and phrasing them as a proof-by-contradiction means we willfully ignore that information.

However, a very nice example is given by this answer over at math.stackexchange.com: https://math.stackexchange.com/a/4619477/128989

The statement is that in the decimal expansion of $\sqrt{2}$ at least two digits occur infinitely often. As this is a positive statement, proving it by deriving a contradiction (via the irrationality of $\sqrt{2}$) is a genuine proof by contradiction. According to Z.A.K., we don't actually have a proof for any particular digit to occur infinitely often, so there is no "willful ignorance" going on either.

On the other hand, The strategy stealing example isn't really working. What strategy stealing shows is "This player does not have a winning strategy", and it is a proof by negation. To get to "The other player has a winning strategy" you also need that the game is determined. Whether the entire argument then is constructive depends on the proof of determinacy.

Answer 2

Refutations by contradiction (a.k.a proof of negation)

The usual proofs of the following statements are refutations by contradiction:

• Euclid's Elements, Book 1, Proposition 6: If in a triangle two angles equal one another, then the sides opposite the equal angles also equal one another.
• Russell's paradox
• $\sqrt{2}$ is irrational
• Infinitude of primes
• Arguments by infinite descent, such as "there is no smallest positive rational"
• Non-existence of the Halting oracle.

Proof by contradiction

The usual proofs of the following statements are proofs by contradiction

• Hilbert's Nullstellensatz
• Infinitude of primes
• Heine-Borel compactness of $[0,1]$ can be proved by contradiction, as in Theorem 11.5.11 at PlanetMath, although it also uses some instance of excluded middle. The subsequent discussion on how to make it more constructive is also relevant.
• The usual proofs of "an epimorphism is surjective" proceed by contradiction: suppose $f : A \to B$ is epi but not surjective, then there is $y \in B \setminus \mathrm{im}(f)$, which allows us to construct $g, h : B \to \{0,1\}$ differing at $y$, so that $g \circ f = h \circ f$. (See this answer for a constructive proof.)
• In a Heine-Borel compacts space $X$, if a family of closed sets $F_i$ has the finite intersection property (every finite intersection is inhabited) then the whole intersection is inhabited: if $\cap_i F_i$ were empty, $X \setminus F_i$ would form an infinite cover of $X$ without a finite subcover.
• If there is no continuous retraction from the unit disk $D^1$ to the unit circle $S^1$ then every continuous map $f : D^1 \to D^1$ has a fixed point: suppose $f : D^1 \to D^1$ were without a fixed point. Then we could define a retraction $D_1 \to S^1$ by mapping $x \in D^1$ to the intersection of $S^1$ and the half-ray with the origin $x$ passing through $f(x)$.

Excluded middle

• König's lemma: an infinite binary tree has an infinite path. Start at the root. The left subtree is either infinite or not. If it is, go left, otherwise go right. Repeat.
• “A subset of a finite set is finite” is equivalent to excluded middle.
• Cantor-Schröder-Bernstein theorem uses excluded middle and implies it. (The proof with the most obvious use of excluded middle is Tarski's proof using the fixed point theorem.)

Answer 3

Here are a few more:

1. The classic nonconstructive proof using excluded middle that "there exist irrational numbers $\alpha$ and $\beta$ such that $\alpha^\beta$ is rational" is just as nice when rephrased as a proof by contradiction. Assuming $\text{irrational}^{\text{irrational}}$ is always irrational, we have that $\sqrt{2}^{\sqrt{2}}$ is irrational, hence so is $(\sqrt{2}^{\sqrt{2}})^{\sqrt{2}} = \sqrt{2}^2 = 2$, a contradiction. (Of course, this theorem also has a different constructive proof.)

2. The pigeonhole principle and its applications can be phrased as proofs by contradiction. Likewise the infinite pigeonhole principle, and its generalization to the infinite Ramsey theorem.

3. The infinite Ramsey theorem implies the finite one.

And since you said in your response to Andrej that you're also interested in proofs using excluded middle, here are some more of those:

1. Trichotomy for real numbers. This is a little tricky to use in an intro-to-proofs class because it requires a definition of "real number", and the standard definitions of real numbers such as Cauchy sequences or Dedekind cuts may not be familiar to students at that level. If you define real numbers as some kind of decimal expansions with a sign bit, then trichotomy may be self-evident, but excluded middle is then necessary to define addition of a negative number and a positive one.

2. The Intermediate Value Theorem, the least-upper-bound property, and the monotone convergence theorem all have "shrinking intervals" proofs that rely at each step on either trichotomy for real numbers or excluded middle (and convergence of Cauchy sequences at the end).

3. Dually to Andrej's "a subset of a finite set is finite", there is "a surjection with finite domain has a section and its codomain is also finite".

4. Every subset of a countably infinite set is either finite or countably infinite.

5. Similarly, any subspace or surjective image of a finite-dimensional vector space is finite-dimensional.