Mathematicians who are finitists.

[A Toy Windmill]

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 first three claims can be expressed as simple equations on a primitive recursive quotient function.

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.

Yes. Here's as much as I'm willing to claim:

Do finistists accept the existence of irrational numbers?

I don't think so, at least not in the sense that everyone else does. The classic proof that a square's diagonal is incommensurable with its side looks finitistic to me, but that's not what a modern mathematician means by "the square root of 2 exists."

The classic proof is just that the square of a rational cannot be 2. This was the only commitment of the classical Greeks and those for followed them, and I don't think they're bad company.

I'm not sure a purely finitistic proof of the existence of sqrt(2) is possible. Anyone?

I'm confident that the standard rational sequence whose squares converge to 2 is finitistically provably such. Again, this isn't as much as a classical mathematician can assert today, which is that there is a unique positive object which squares to 2 in any interpretation of the axioms of closed ordered fields, of which Dedekinds cuts are an example.