Mathematicians who are finitists.

[A Toy Windmill]

OK, so this particular unbounded quantifier is allowed? Why is that? Are quantifiers of the form
for all n>=p, P(n)
allowed?

Quantifiers are allowed if they're all outermost. Such quantifiers are then dropped, and you're left with a statement that just has free variables.

When every statement in every proof has this form, you can treat them all as schema or templates. That means that, for my proof above, if someone has concrete numerals for the numerator and denominator of ε, I can plug them in and run that proof down to applied axiom schemes for primitive recursive arithmetic.

I can't do this if quantifiers ever appear left of an implication, as in, say, the principle of mathematical induction:

for any property P, if P holds of 0, and holding of n implies holding of (n+1), then P holds for all natural numbers.

Primitive recursive arithmetic cannot have this as an axiom, because the quantifier position is illegal. Instead, it takes induction as an inference rule.