Mathematicians who are finitists.

[Jehanne]

I'm familiar with the proof. It looks easy enough to formalize in PRA.

Where do you think it requires unbounded quantification over the naturals?

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.  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.  But, consider the harmonic series:



It goes on forever, but, as can be proved, it is unbounded (goes to infinity), even though though the terms of the series (its limit) goes to zero.  The sum of a p-series, where p > 1



is bounded, even though it, like the harmonic series, goes on forever.

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!