Does finitism allow $\exists$- Introduction Rule which says that if $x$ is not free in $\psi$, infer $\exists x\phi\rightarrow\psi$ from $\phi\rightarrow\psi$?
As far as I know, finitist would not accept quantification over infinite domains. If finitist accept $\exists$-Introduction Rule, then what does the rule mean for finitist?
Thank you.