如何构造性证明素数的无穷性？关于证明中排中律应用的疑问

我之前碰到过类似的问题，但那些答案都没法完全解决我的困惑。

在素数无穷性的经典证明里，我们会用到“n+1一定存在一个素因子”这个结论。我平时用经典逻辑的思路来证这一点：如果n+1本身是素数，那它自己就是这个素因子；如果n+1不是素数，那它必然有一个非平凡因子，再通过归纳法就能推出这个因子存在素因子。

但这个证法看起来用到了排中律的假设——也就是$p(n+1) \lor \lnot p(n+1)$，这里的$p(x)$代表“x是素数”的命题。

不过我总觉得这个证明应该是符合构造性要求的，毕竟判断一个数是不是素数是可以有效计算的——只要遍历所有小于它的数对，检查是否存在能整除它的数就行。不过哪怕我们已经证明了$p(x)$等价于一个带“有界量词”的命题，我还是有一些没理清的地方...

备注：内容来源于stack exchange，提问作者antilope