Mathematicians who are finitists.

[A Toy Windmill]

What's the alternative?  I suppose that you, as the DA, are trying to make a distinction between a potential infinite versus an actual one.

I'm not playing Devil's Advocate. This is not a debate. Either the classical proof of the irrationality of the square root of 2 is a theorem of PRA or it isn't. I'm confident that it is, and the matter can be settled definitively by providing the formalized proof. It could even be checked by a machine.

But, here's the Axiom of Infinity:



Wikipedia -- Axiom of Infinity

Now, if one rejects the above axiom, then, one, I suppose is a finitist.

Finitism has stronger constraints. ZF set theory without the axiom of infinity is as expressive as Peano Arithmetic, which is strictly more expressive than primitive recursive arithmetic.

But, consider the harmonic series:

Why are we moving away from the proof that there is no rational square root of 2? I know there are classical theorems that are not provable by finitistic methods. But you seem to be under the mistaken impression that finitism is far weaker than it is. The article I linked early discusses a paper which claims that the majority of contemporary mathematics is formally provable by finitist methods.

I am not sure how finitists deal with the above conundrums, but, of course, if you tire in your role as the DA here, I understand completely!

Statements about convergence can be finitistic. Even classically, a convergence statement about a series that converges as n goes to infinity is formalized as:

for any ε > 0, I can produce N such that f(n) - l < ε for all n > N.

Many such statements can be proven finitistically. You just need a primitive recursive procedure that sends the ε to the N. The "for any" and "for all" can both be moved outermost, so the quantification here is one that a finitist accepts.