背理法がどうのこうのについて

背理法、P を前提にして矛盾を導いて ¬P を言うっていう理解が多すぎると思うんだけど、
こんなもんまで問題にするのはそれこそ問題であって、これは否定の導入だとか含意の導入だとか言えばいい。ここらへんまで認めないのは直観主義よりもさらにアレなのでアレである。
よくある√2が無理数であることの証明なんて、少なくとも高校での無理数の定義（有理数でないこと）から考えればこちらの場合に属するので背理法でもなんでもない。

¬P を前提にして矛盾を導いて P を言うっていうんであればそこは何か問題の本質に踏み込んでいるので意味がある。これは背理法だ。二重否定除去と言ってもいい。

そこらへん区別してないもんが多すぎる気がする。