背理法、P を前提にして矛盾を導いて ¬P を言うっていう理解が多すぎると思うんだけど、 こんなもんまで問題にするのはそれこそ問題であって、これは否定の導入だとか含意の導入だとか言えばいい。ここらへんまで認めないのは直観主義よりもさらにアレなので…