Nonetheless, mathematician (and Fields medal winner) Tim Gower has an entertaining dialogue on whether you can prove the existence of the square root of two.
I like the idea that for any non-rational number you can define an ever-decreasing interval that appears to converge on the number. For example, take any finite decimal expansion of root 2. This will be slightly lower than the fully expanded number. Then add 1 to the digit at the very right hand side. This will give a number slightly higher than the fully expanded number. Thus for any finite expansion whatever, you can define an interval which contains root 2. For example, the interval
[1.4142135623, 1.4142135624]Furthermore, for any such interval you can find the next digit in the expansion, and define in interval which lies completely inside the first interval, and which also contains root 2. For example, we know that the next digit in the expansion above is 7. Thus the interval
[1.41421356237, 1.41421356238]contains root 2, and lies inside the first interval.
Thus we can prove the existence of an infinite set of intervals each of which contains root 2, and each of which can be further subdivided into another such subinterval inside that, and so on and so on. But does that prove the existence of root 2 itself, which is not an interval, and which is 'indivisible'? That is precisely where I lost Gowers' argument (the bit right at the end, where the disputant appears to accept the idea that you can define something into existence).
[Added as an afterthought. I have a paper somewhere by Bolzano, written in 1917, where he attempts to prove by logic the intermediate value theorem. It is blatantly fallacious, although a part of it eventually turned into the Bolzano-Weierstrass theorem. This must be connected in some way, but it's so long ago I've forgotten most of it. Could we not say, for example, that there are two sequences implied in the example above, one of increasing numbers that approach root 2 'from below', and the other of decreasing numbers which approach if 'from below'? ]