I wrote an Email to my Logic professor, asking him what the relativisation of a formula wrt. a formula was. Unfortunately, he said he wouldn't tell by mail. Thus, I have to turn to the internet community and kindly ask for a definition.
Namely, suppose we have to formulae $\varphi$ and $\psi$ over a certain formal language. What then is the symbol $$ \varphi^\psi $$ supposed to mean? Is there a definition that is analogous to the one of the relativisation wrt. a class? Note that both formulae are permitted to have several arguments.
Thanks in advance.
I have been able to figure it out. Namely, we quantify over the class of symbols that satisfy the first argument of the formula, when the other arguments are filled with variables that need to be passed to $\varphi^\psi$.