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$. All I can do is tell you that there should be such an argument.
$\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.)