HN Debrief

Making Sense of Proof by Contradiction [pdf]

  • Mathematics
  • Logic
  • Education

The PDF is a short pedagogical piece about why proof by contradiction feels slippery even though students learn to use it early. It uses familiar examples like the irrationality of √2 and Euclid-style prime arguments to show the pattern of assuming the opposite of what you want, reaching an impossibility, and concluding the target claim. The strongest reaction was that this blurs together several different proof moves that happen to end in a contradiction. People drew a clean line between proving a negation by assuming the positive and deriving absurdity, proving a contrapositive, and proving a positive statement by assuming its negation and then using double-negation elimination. That last step is the one that needs classical logic. The earlier forms do not.

If you teach, write, or formalize proofs, stop lumping every "assume X and derive absurdity" argument together. The practical line is whether you only proved a negation, proved a contrapositive, or used double-negation elimination to recover a positive claim, because that is where constructive proof assistants and non-classical logics start to differ.

Discussion mood

Mostly engaged and corrective. People liked the teaching goal, but many thought the note muddies an important distinction between ordinary contradiction arguments and the specifically classical move from not-not-P to P, then got hung up on terminology and what students are actually missing.

Key insights

  1. 01

    Euclid-style examples are constructive proofs

    Euclid’s prime argument and similar textbook examples do more than show an assumption is impossible. They produce a witness or method. If someone claims to have listed all primes, the argument constructs a new prime from that list. That shifts the example out of the controversial territory. The non-constructive step is not deriving absurdity itself. It is deriving a positive claim from the impossibility of its negation.

    When choosing examples for proof assistants, constructive math, or teaching, separate witness-producing arguments from arguments that only eliminate alternatives. If an example builds an object or procedure, present it as constructive proof first and only secondarily as a contradiction-flavored argument.

      Attribution:
    • butokai #1
    • dwenzek #1
    • sxzygz #1
  2. 02

    The real fault line is double negation

    The clean operational test is whether the proof needs double-negation elimination. Showing ¬P by assuming P and deriving absurdity works fine constructively. Showing P by assuming ¬P and deriving absurdity only gets you ¬¬P, and the extra step to P is exactly where classical logic enters. That framing is more useful than arguing over labels, because the same proof can be harmless or non-constructive depending on where that conversion happens.

    If you are porting mathematics into Lean, Coq, or another proof system, look for uses of ¬¬P ⇒ P instead of searching for the phrase "by contradiction." That will find the actual places where classical axioms are doing work.

      Attribution:
    • dhosek #1
    • MaxRegret #1 #2
    • saithound #1 #2
  3. 03

    Hidden consistency assumptions are what confuse students

    Student discomfort is not just about syntax. A contradiction only tells you that some assumption set is inconsistent. In informal proofs, the temporary assumption gets blamed immediately, but that inference quietly depends on the rest of the background theory being consistent. Commenters argued this missing premise is what makes classroom explanations feel hand-wavy. The article notices the discomfort but stops before making that metalogical dependency explicit.

    If you are teaching or documenting a contradiction argument, state the trusted background assumptions out loud. That small move makes the conclusion feel earned instead of magical, especially for people new to hypothetical reasoning.

      Attribution:
    • jerome-jh #1 #2
    • calf #1 #2

Against the grain

  1. 01

    Restricting the term is revisionist

    Several commenters rejected the attempt to reserve "proof by contradiction" for only the classical pattern that proves a positive by refuting its negation. They argued that mainstream mathematical usage has long applied the phrase to any argument that begins "suppose for contradiction" and ends in absurdity. On this view, the newer narrow definition is useful in some logic circles, but it is not standard language and can create more confusion when talking to ordinary mathematicians.

    If you write for mixed audiences, define your terminology instead of assuming your preferred distinction is shared. You can keep the logical distinction without starting a naming fight that obscures the proof itself.

      Attribution:
    • loicd #1
    • saithound #1
  2. 02

    Reductio works beyond bivalent logic

    One line of pushback said the core reductio move does not depend on the law of the excluded middle at all. Showing that an assumption leads to absurdity can still rule out that assumption in trivalent or other non-classical logics. What fails outside classical logic is the extra jump from "not not P" to "P." That narrows the scope of the classical commitment more than many textbook presentations do.

    Do not treat every contradiction-based argument as evidence that your reasoning is fully classical. You may be able to keep the structure of the proof in a weaker logic and only isolate the final classical step, if there is one.

      Attribution:
    • adrian_b #1 #2 #3

In plain english

classical logic ↩
The standard logic used in most mathematics, which accepts principles like the law of the excluded middle and double-negation elimination.
constructive logic ↩
A family of logics that only accepts proofs that effectively build or demonstrate what they claim, and usually rejects some classical principles.
contrapositive ↩
For a statement "if P then Q," the logically equivalent statement "if not Q then not P."
double-negation elimination ↩
The classical logic rule that lets you infer P from ¬¬P.
law of the excluded middle ↩
A classical logic principle stating that for any statement P, either P or not P must hold.
metalogical ↩
About the properties and assumptions of a logical system itself, rather than statements made inside that system.
P ⇒ ⊥ ↩
Logical notation meaning "if P then absurdity," a common way to define not-P.
¬P ↩
Logical notation for "not P," meaning the statement P is false or leads to contradiction depending on the logic used.
¬¬P ↩
Logical notation for "not not P," meaning it is impossible that P is false.

Reference links

Logic terminology and proof style

Constructive mathematics references

  • Myths about constructive mathematics
    Used to show that established constructive mathematicians still describe the √2 irrationality proof as proof by contradiction.
  • locrcg.pdf
    Another reference offered to show mainstream usage of the phrase among researchers close to constructive and logical foundations.