(July 5, 2019 at 1:33 am)A Toy Windmill Wrote:(July 4, 2019 at 6:46 pm)Jehanne Wrote: The proof of the irrationality of the square root of 2 by contradiction is what I had in mind, anything but finitism in my opinion.That proof looks straightforwardly finitistic to me. Where do you think it requires quantification over all the natural numbers?
Well, you need to know that the square of every even number is even, that the square of every odd number is odd, that every natural number is either even or odd, and that irrationality is the non-existence of two natural numbers x,y with x^2 =2 y^2.
The last quantification is probably the one that breaks the proof since I don't see how to get by with just bounded quantification in it.
Another aspect of this is that the existence of sqrt(2) is not guaranteed. All this proof does is show that it cannot be rational.
I'm not sure a purely finitistic proof of the existence of sqrt(2) is possible. Anyone?