-1

The proof of various theorems are nowadays routinely described as "proof by contradiction".

For example, the following theorems:

https://en.wikipedia.org/wiki/Proof_by_contradiction

  • The square root of 2 is irrational.

  • In any non-degenerate right triangle, the length of the hypotenuse is less than the sum of the lengths of the other two sides.

  • There is no smallest rational number greater than 0.

The "proof by contradiction" is always formally expressed by the following formula:

A → (B ∧ ¬B) ⊢ ¬A

In the logical tradition, the terminology used was as follows:

https://en.wikipedia.org/wiki/Reductio_ad_absurdum

  • demonstration to the impossible (Aristotle)

  • reductio ad absurdum (Latin for "reduction to absurdity")

  • argumentum ad absurdum (Latin for "argument to absurdity")

  • apagogical argument (argument in which the conclusion is arrived at through the disproving of its contradiction)

  • the appeal to extremes

So, when did this notion of proof by contradiction appear first, and who was the logician or mathematician who was the first to see the formula A → (B ∧ ¬B) ⊢ ¬A as the logical principle underlying the proof of some mathematical theorems?

When did this notion that a proposition that implies a contradiction is necessarily false appeared first in the history of formal logic?

Improve this question
15
  • 2
    The question is how much of what goes into this formula you want to count. Aristotle did not have propositional connectives, so he mostly dealt with the special case A → ¬A ⊢ ¬A, and A of a very special form. In mathematics, reductio goes back to Pythagoreans, but detaching the logical form, using connectives, and then thinking of a proof as instantiating that, probably did not occur before Leibniz. Only Peirce and Frege brought in quantifiers, so A and B could be of general form, but even they did not separate → and ⊢ clearly. It was more like A ⊢ B, A ⊢ ¬B ⊢ ¬A. Nobody was "first".
    – Conifold
    Commented Sep 14, 2019 at 5:33
  • 1
    Is this good enough? "For all who effect an argument per impossibile infer syllogistically what is false, and prove the original conclusion hypothetically when something impossible results from the assumption of its contradictory" Prior Analytics, I.23. Meanings of "proposition" and "necessarily" underwent some major transformations, in the last 200 years especially. By the time it was stated with modern meanings (in modern textbooks) it was already a platitude. If you are looking for a time when it was novel you'll have to be flexible.
    – Conifold
    Commented Sep 15, 2019 at 0:31
  • 1
    Those who stated it in the modern form were not first because it was already a platitude. Those before them were not first because they did not state it this way. The path between was by incremental morphing of concepts and conceptions. Where it became "modern enough" is a subjective judgment, and you'll have to pour through 20th century textbooks to make it to your personal satisfaction. In a more substantive sense, the answer to who was "first" to set up some modern formulation is, typically, nobody. It is a process with multiple people contributing increments. Not just on this.
    – Conifold
    Commented Sep 15, 2019 at 8:49
  • 1
    At least now you know why this question, and similar ones, will not be answered. But there are more historically aware ones around it that can be. Pick your poison.
    – Conifold
    Commented Sep 15, 2019 at 9:45
  • 1
    It is the same with "who was first to discover irrational numbers", "who was first to design a ruler", etc. We generally advise users on hsm to ask "what were the early occurrences of X" instead, and avoid distinctly modern formulations for X. I was serious, you may find what satisfies you by going over Principia, Hilbert-Ackerman, Mendelsohn, and lesser known textbooks in chronological order, but, with your formulation, this is not something that would be marked by historians as significant and appear in the secondary literature.
    – Conifold
    Commented Sep 16, 2019 at 6:55

2 Answers 2

Reset to default
1

Euclid's Proposition 20 in Book IX of the Elements claim

Prime numbers are more than any assigned multitude of prime numbers.

David E. Joyce provides the following outline of the proof:

Suppose that there are n primes, a1, a2, ..., an. Euclid, as usual, takes an specific small number, n = 3, of primes to illustrate the general case. Let m be the least common multiple of all of them. (This least common multiple was also considered in proposition IX.14. It wasn’t noted in the proof of that proposition that the least common multiple of primes is their product, and it isn't noted in this proof, either.)

Consider the number m + 1. If it’s prime, then there are at least n + 1 primes.

So suppose m + 1 is not prime. Then according to VII.31, some prime g divides it. But g cannot be any of the primes a1, a2, ..., an, since they all divide m and do not divide m + 1. Therefore, there are at least n + 1 primes. Q.E.D.

The OP asks

So, when did this notion of proof by contradiction appear first, and who was the logician or mathematician who was the first to see the formula A → (B ∧ ¬B) ⊢ ¬A as the logical principle underlying the proof of some mathematical theorems?

This answer addresses the first part of the question. Mauro ALLEGRANZA's post answers the second part referencing Aristotle as the first logician to note this principle.

Euclid's proof that there is no assigned multitude of prime numbers uses this notion of proof by contradiction. A is the assumption that there is an assigned multitude of primes. Call it n. The least common multiple of these primes represent either a larger prime or a prime divisor larger than any in the least common multiple. That contradicts A, so A is rejected.

The use of proof by contradiction in mathematical theorems goes back at least as far as Euclid.

Joyce, D. E.. Clark University (1998) Retrieved on September 13, 2019 from https://mathcs.clarku.edu/~djoyce/java/elements/bookIX/propIX20.html

Improve this answer
2
  • Thanks. Yes, I'm aware of what Aristotle said on the subject but I'm interested specifically in the notion that A → (B ∧ ¬B) ⊢ ¬A is the expression of the principle of proof by contradiction, that is, the notion that a proposition (A) that implies a contradiction (B ∧ ¬B) is necessarily false (¬A).
    – Speakpigeon
    Commented Sep 13, 2019 at 14:03
  • @Speakpigeon For the history of this inference rule in natural deduction I imagine this would have originated with Gerhard Gentzen en.wikipedia.org/wiki/Gerhard_Gentzen#Work
    – Frank Hubeny
    Commented Sep 13, 2019 at 16:01
1

For sure, we can find it in Aristotle :

In the proofs for imperfect deductions [the syllogistic figures different from the fist one], Aristotle says that he “reduces” (anagein) each case to one of the perfect forms [the first figure] and that they are thereby “completed” or “perfected”. These completions are either probative (deiktikos: a modern translation might be “direct”) or through the impossible (dia to adunaton).

A completion or proof “through the impossible” shows that a certain conclusion follows from a pair of premises by assuming as a third premise the denial of that conclusion and giving a deduction, from it and one of the original premises, the denial (or the contrary) of the other premises. This is the deduction of an “impossible”, and Aristotle’s proof ends at that point. An example is his proof of Baroco in Prior An.,27a36–b1.

See Reductio ad absurdum: "this technique is traced back to classical Greek philosophy in Aristotle's Prior Analytics (62b, Greek: ἡ εἰς τὸ ἀδύνατον ἀπόδειξις, lit. 'demonstration to the impossible')".

See alo Reductio ad Absurdum.

Improve this answer
1
  • Thanks. Yes, I'm aware of what Aristotle said on the subject but I'm interested specifically in the notion that A → (B ∧ ¬B) ⊢ ¬A is the expression of the principle of proof by contradiction, that is, the notion that a proposition (A) that implies a contradiction (B ∧ ¬B) is necessarily false (¬A).
    – Speakpigeon
    Commented Sep 13, 2019 at 14:01

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .