Если к этому серьёзно подходить, то надо зафиксировать логику и теорию, в рамках которых ищется доказательство. Скажем, можно взять логику первого порядка с естественным выводом и аксиомы Пеано, зафиксировать для удобства кучу теорем (типа свойств чётности), и думать про выводимость иррациональности из всего этого без использования конкретного правила вывода. Только тогда иррациональных чисел не будет, а то, что вообще можно сформулировать в арифметике (
![$\neg \exists m, n \enskip m^2 = n^2 + n^2 \wedge ( m \neq 0 \vee n \neq 0)$ $\neg \exists m, n \enskip m^2 = n^2 + n^2 \wedge ( m \neq 0 \vee n \neq 0)$](https://dxdy-02.korotkov.co.uk/f/d/8/b/d8be0d2779edc99e3244ab769e11074682.png)
) доказывается без "от противного", как уже несколько раз упоминалось.