つづき

＜仏語（仏語ダメなので英訳スイッチ入れた）＞
https://fr.wikipedia.org/wiki/Raisonnement_par_l%27absurde
(google英訳)
Proof by contradiction

In logic and mathematics
In mathematical logic , we distinguish the rule of refutation [ref. needed] :
・p → False, therefore not( p ) , which can be taken as the definition of negation .
of the rule of reasoning by contradiction :
・not( p ) → False, therefore p is proof by contradiction.
Both classical and intuitionistic logic admit the first rule, but only classical logic admits the second rule, which involves the elimination of double negatives [citation needed] . Similarly, the law of excluded middle is rejected in intuitionistic logic . Therefore, no proof in intuitionistic logic can rely on proof by contradiction. In other words, any proposition provable in intuitionistic logic can be proven without using it. Conversely, a proposition demonstrable in classical logic but not demonstrable in intuitionistic logic requires proof by contradiction [citation needed] .

Examples and counter-examples
・Proof of the irrationality of √2 : We assume that √2 is rational. Therefore , there exist two integers a and b, which we can assume to be coprime , such that √2 =a/b
We then have 2b² = a² . If we take the remainders of both sides in the division by 2, we obtain a² = 0 mod 2 , so a is even and equal to 2a ' ( where a ' is an integer). We then have b² = 2a'² , which, by a comparable line of reasoning, leads to b being even . However , the fact that a and b are both even leads to a contradiction with a and b being coprime. The statement √2 is rational then leads to a contradiction, and therefore its negation is valid: √2 is irrational.
In this proof, we have only used the fact that if a proposition P leads to a contradiction, then not( P ) is true .
There is therefore no proof by contradiction, despite appearances.
The reasoning presented is thus valid in both classical and intuitionistic logic.
(引用終り)
以上