Writing $\forall q\, (\forall p\,q)$ instead of the schematic $\forall p\,\phi$

Question

Suppose we're working with the propositional logic enriched with propositional quantifiers. Is it, in general, all right to write $\forall q\, (\forall p\,q)$ instead of the schematic $\forall p\,\phi$? Consider, for example, the Universal Instantiation rule: $\forall\!p\,\phi\to\phi[\psi/p]$. Would it be grammatical to turn this schematic axiom into something like this: $\forall q\forall r\, ((\forall p q)\to q[r/p])$?

Answer 1

With the usual definitions, this won't work. The difficulty is that, unlike $\phi$, which can contain occurrences of $p$ for you to replace with $\psi$, the propositional variable $q$ doesn't contain any occurrence of $p$ for you to replace with $r$.

It might be possible to invent some new notion of substitution to make this idea work, but I don't see a reasonable way to do that (and I'm quite skeptical about the possibility).