On a somewhat technical note, I think the author is being slightly imprecise, though in a way that will normally not trip up most people. The proof has to be understood either as a proof scheme in first order logic, in which case we technically need a separate proof for each possible choice of predicates P and Q, or we have to implicitly quantify over P and Q, i.e. "for all P, for all Q", which leads us to second order logic, but in this case there is now a single proof (which is exactly what's the case when we're using Coq).
At least that's the case in classical logic (which is enough to understand this article), I'm not knowledgeable enough about intuitionism to know whether it typically includes second-order quantification, but even in that it would probably be better to make the quantification explicit.
Comments
On a somewhat technical note, I think the author is being slightly imprecise, though in a way that will normally not trip up most people. The proof has to be understood either as a proof scheme in first order logic, in which case we technically need a separate proof for each possible choice of predicates P and Q, or we have to implicitly quantify over P and Q, i.e. "for all P, for all Q", which leads us to second order logic, but in this case there is now a single proof (which is exactly what's the case when we're using Coq).
At least that's the case in classical logic (which is enough to understand this article), I'm not knowledgeable enough about intuitionism to know whether it typically includes second-order quantification, but even in that it would probably be better to make the quantification explicit.