>>112 補足
>Refutation by contradiction
>In contrast, proof by contradiction proceeds as follows:

下記 en.wikipediaでは √2の無理数証明は、
上記の ”Refutation by contradiction”で、”(and therefore are intuitionistically valid)”
だとある
後述の 仏語 Proof by contradictionでも同様で √2の無理数証明は
”There is therefore no proof by contradiction, despite appearances.
The reasoning presented is thus valid in both classical and intuitionistic logic.”
とある

国際的には √2の無理数証明は厳密には背理法でなく ”Refutation by contradiction”であって
”thus valid in both classical and intuitionistic logic”とあります
いやはや、背理法被害者の会の人、これ知ってるんかな？ （＾＾

(参考)
https://en.wikipedia.org/wiki/Reductio_ad_absurdum
より
Examples of refutations by contradiction
The following examples are commonly referred to as proofs by contradiction, but formally employ refutation by contradiction (and therefore are intuitionistically valid).[38]
（(google訳追加)以下の例は一般的に背理法による証明と呼ばれていますが、形式的には背理法による反駁を採用しています（したがって直観主義的に妥当です）。[ 38 ]）

Irrationality of the square root of 2
The classic proof that the square root of 2 is irrational is a refutation by contradiction.[39] Indeed, we set out to prove the negation ¬ ∃ a, b ∈ N.
a/b = √2 by assuming that there exist natural numbers a and b whose ratio is the square root of two, and derive a contradiction.

Assume that √2 is rational,[40] so it can be written as a fraction a/b in lowest terms, where a and b are integers with no common factors. This assumption allows us to apply a proof by contradiction.[41] Squaring both sides gives 2 = a²/b², which implies that a² = 2b².[42] Therefore, a² is even, and it follows that a must also be even. Let a = 2k for some integer k. Substituting back into the equation gives (2k)² = 2b², which simplifies to 4k² = 2b², or b² = 2k². Hence, b² is even, and therefore b must also be even. This shows that both a and b are even, which contradicts the assumption that a/b was in lowest terms. Therefore, the original assumption is false, and √2 is irrational.[40]

Proof by infinite descent
略

つつく