>>685
>太田：お〜い、田中、古典論理の ZFC の論理体系では
>排中律や二重否定の使用は認められているが、
>直観主義的敵論理の論理体系では
>排中律や二重否定の使用が認められていないから、

その話は、下記 ”背理法は不要なのか”スレでも議論したが
下記 en.wikipedia Reductio ad absurdum 「背理法」を見ておくれ

2の平方根の無理性の典型証明は、
俗な分類では背理法だが
英語では refutations by contradictionで あって
直観主義的にも妥当だよ（常識らしいから 覚えておいてね）

(参考)
https://rio2016.5ch.io/test/read.cgi/math/1781354251/41
背理法は不要なのか
https://rio2016.5ch.io/test/read.cgi/math/1784536028/
背理法は不要なのか2

https://en.wikipedia.org/wiki/Reductio_ad_absurdum
Reductio ad absurdum 背理法
(一部 google訳)

Relationship with other proof techniques
Refutation by contradiction （矛盾による反駁）
Proof by contradiction is similar to refutation by contradiction,[30][31]
Formally these are not the same, as refutation by contradiction applies only when the proposition to be proved is negated, whereas proof by contradiction may be applied to any proposition whatsoever.[32]

Examples of refutations by contradiction
以下の例は一般的に背理法による証明と呼ばれていますが、形式的にはrefutation by contradictionを採用しています（したがって直観主義的に妥当です）。[ 38 ]
（原英文）
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]

2の平方根の無理性
2の平方根が無理数であることの古典的な証明は、背理法による反駁である。[ 39 ]実際、我々は否定¬ ∃ a, b ∈N を証明しようとした。
a/b = √ 2 は、比が 2 の平方根となる自然数aとbが存在すると仮定して、矛盾を導きます。
（原英文）
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.