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.
  • 2
    $\begingroup$ Could you start us off, by extracting the answers that do meet the criteria, from previous question, and listing them? You say most did not, but that means some did, right? Unless "all" is included in "most"...not sure the logic, here. ;) I have a little concern that there's an equivalence here in what you are distinguishing, but my Boolean algebra and logic is VERY limited, so it is just a concern, not an assertion. $\endgroup$ Commented Jan 8, 2023 at 16:26
  • 1
    $\begingroup$ A constructive mathematician makes a distinction between $\neg(\neg p)$ and $p$ which a classical mathematician does not make. I am not a constructivist for any philosophical reasons, but I find that I produce cleaner arguments when I pay attention to whether my work is constructively or classically valid. $\endgroup$ Commented Jan 9, 2023 at 14:01
  • 2
    $\begingroup$ Just to check whether I understand the notions correctly: the classical Euclid proof of the fact that there are infinitely many primes is a proof by contradiction. However the very same proof of the statement that it is not true that primes are finitely many would be a proof by negation, and constructive mathematics makes a distinction between "the primes are infinitely many" and "the primes are not finitely many", right? $\endgroup$
    – fedja
    Commented Jan 10, 2023 at 18:41
  • 2
    $\begingroup$ I'm not sure what your question is. $\endgroup$
    – user18187
    Commented Jan 16, 2023 at 3:38
  • 3
    $\begingroup$ @StevenGubkin: even if you write just for constructivists, you should mention that the prevalent usage of "proof by contradiction" means "any argument that arrives at contradiction" (which includes proof of negation). Only constructivists seem to be using "proof by contradiction" in the narrower sense. $\endgroup$ Commented Jan 17, 2023 at 9:17

2 Answers 2


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.

  • $\begingroup$ I agree that this is a nice example! I hope we can find more examples of an elementary character. $\endgroup$ Commented Jan 16, 2023 at 16:14
  • $\begingroup$ @Steven Gubkin: The examples in my answer to Examples and applications of the pigeonhole principle are similar, especially the 3rd which is a trivial generalization of the example Arno gives. $\endgroup$ Commented Jan 16, 2023 at 18:19

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.)
  • $\begingroup$ Thanks for this answer! Your examples of proof by contradiction are (with the exception of the infinitude of primes) a little too advanced for my "intro proof" audience I am afraid. If you think of any really elementary arguments which fit please update! $\endgroup$ Commented Jan 17, 2023 at 12:15
  • 1
    $\begingroup$ I can think of some simpler ones that use excluded middle, as opposed to proof by contradiction. Are you interested in those? $\endgroup$ Commented Jan 17, 2023 at 15:54
  • $\begingroup$ Yes, would definitely be interested! They would be useful for the excluded middle section, and could maybe be retooled into proof by contradiction examples. $\endgroup$ Commented Jan 17, 2023 at 16:52
  • $\begingroup$ I added a table of "sacrifices" to the end of my question. Hoping you might give me your advice on whether I have gotten these correct, and also examples of proofs by contradiction which highlight these other potential sacrifices. $\endgroup$ Commented Feb 22, 2023 at 22:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.