Getting rid of quantifiers over functions

Question

This is a followup to this question, and I'm in general trying to better understand under what conditions it is possible to find simplified equivalent formula's for a complex formula. It is possible to prove the equivalence between the following two formulas (using the axiom of choice):

$$\begin{align} &\text {some sets }A,B\\ &\forall f:A\to B, [\forall a,P(a,f(a)) \to \forall a,Q(a,f(a))]\tag 1&\\ &\forall a\forall b,[P(a,b)\to Q(a,b)]&\quad \text {where}\tag 2\\ &P:A\times B \to \{T,F\}\\ &Q:A\times B \to \{T,F\} \end{align}$$

Essentially, the first equation quantifies over functions, but we can use the axiom of choice to get rid of quantification over $f$, and talk only directly about $a$'s and $b's$. This is nice because functions are "unnecessarily complicated" in this case, so the second formula is much simpler.

I am trying to understand when it is and when it is not possible to remove quantifiers over functions like this. Obviously, it would not be possible for the following formula:

$$\forall f:A\to B, [\forall a,\tilde P(a,f) \to \forall a,\tilde Q(a,f)]$$ If $\tilde P(a,f)$ and $\tilde Q(a,f)$ are arbitrary (i.e. we know nothing about them). However, I'm not so sure if it's still impossible for a proposition like the following:

$$\begin{align} &\forall f,g:A\to B,[ \{\forall a,P(a,r(f,g)) \}\to\{\forall a,Q(a,r(f,g)))\}]\tag 3\\ &r:(A\to B)\times (A\to B)\to B \end{align}$$

Where we instead know everything about $r$, i.e. we know the exact function $r$. In this case, it seems like we should be able to use this complete information about $r$ to "triangulate" and get rid of the quantifiers over $A\to B $. But I'm not sure, and don't know how to find out. (Maybe it is possible for some $r$ and not others, or iff $r$ is computable, or something like that).

I am similarly unsure for a formula like this:

$$\begin{align} &\forall f:A\to B,[ \{\forall a,\bar P(r(f,k(a))) \}\to\{\forall a, \bar Q(r(f,k( a)))\}]\tag 4\\ &r:(A\to B)\times (A\to B)\to B\\ &k:A\to (A\to B)\\ &\bar P,\bar Q:B\to \{T,F\} \end{align}$$

So I have two questions:

Question 1. Is there an example of a formula of form $(3)$ or $(4)$ or similar (with quantifiers over functions, and complete information of how those functions reduce to properties over the underlying sets), where we provably cannot reduce it to a formula without quantifiers over functions?

Question 2. Is there a topic in math/logic that I can look at that would clarify this for me? (i.e. the problem of turning formula's containing quantifiers over $A\to B$ into one containing only quantifiers over $A$ and $B$). Is there a generally accepted name for this problem/topic, or something related?

Edit: It seems to me that the trick that @MeesdeVries did, cannot be applied to this formula:

$$\forall f:A\to B,\exists \bar a, \{\forall a, P(\bar a, r(f,k(a))) \}\to\{\forall a, Q(\bar a, r(f,k( a)))\}]\tag 5$$

Answer 1

Your (3) is equivalent to $$ \forall b \in \mathrm{im}(r)(\forall aP(a, b) \implies \forall aQ(a, b)), \tag{*} $$ because if your (3) is true, then to prove my (*) for $b$ just choose $f, g$ with $r(f, g) = b$; while if your (3) is false, then if $f, g$ are functions that prove it false, $b = r(f, g)$ will prove my (*) false.

Of course, defining $\mathrm{im}(r)$ requires an existential quantifier over functions, and that might not actually be better as far as you're concerned.

Your second question is almost impossible to answer without specifying it down a little bit, but you might be interested in the study of quantifier complexity (which surprisingly does not have a Wikipedia page, although you can look at the page for the arithmetical hierarchy).