117です。素人のスレ違い気味な質問にいろいろ意見をくださってありがとうございます。

「√2が無理数」という証明では、排中律を認める体系(中高数学ではこういって差し支えないと思いますが)では
>>137,139さんのおっしゃる通り、√2が有理数として矛盾　→　√2は無理数と結論できると思います。

一方で>>135さんのおっしゃった直観主義数学においては二重否定の除去ができないことより
「√2が有理数でない」ことと「√2が無理数であること」は同値ではない
(√2が無理数であることを直接証明により証明しないと真と認めない)ということになると思います。

ですが排中律を認める場合でも、√2が有理数でないことを証明しただけで、√2は無理数である(無理数だとしても矛盾を生じない)と安心して
使っているのに違和感を覚えまして…　まあそれが排中律を認める、ということに他ならないんでしょうが。

体系の無矛盾性などの議論は抽象的でよくわかっていない部分もありますが興味深いことがたくさんありますね…勉強のしがいがあります。