>√2は単に x^2-2=0 の根であるということを意味する記号として扱える。
>実際、数学の証明を書く場合にも、その正確な値を書くことなんてしないし、

例えばC言語は10桁目で四捨五入するようになっていると仮定する。
√xと√yは18桁目までは同じで、19桁目から違う数になるとする。
するとC言語では√x==√yとなってしまう。
√○を記号として扱おうがこれは避けることの出来ないものだ。
するとC言語では実数の大小関係が確定できないことになる。
大小関係が確定できないということは、実数における命題のほとんど全ては
証明することができないことになる。