Techniques for Reversing the Order of Quantiﬁers
Reversal of quantifiers is an important property that is often behind well known theorems.

For example, in analysis the difference between $\forall \epsilon &gt; 0 . \forall x . \exists \delta &gt; 0$ and $\forall \epsilon &gt; 0 . \exists \delta &gt; 0 . \forall x$ is the difference between pointwise and uniform continuity. A well known theorem says that every pointwise continuous map is uniformly continuous, provided the domain is nice, i.e., compact.

In fact, compactness is at the heart of quantifier reversal. Consider two datatypes $X$ and $Y$ of which $X$ is overt and $Y$ is compact (see below for explanation of these terms), and let $\phi(x,y)$ be a semidecidable relation between $X$ and $Y$. The statement $\forall y : Y . \exists x : X . \phi(x,y)$ can be read as follows: every point $y$ in $Y$ is covered by some $U_x = \lbrace z : Y \mid \phi(x,z) \rbrace$. Since the sets $U_x$ are "computably open" (semidecidable) and $Y$ is compact there exists a finite subcover. We have proved that
$$\forall y : Y . \exists x : X . \phi(x,y)$$
implies
$$\exists x_1, \ldots, x_n : X . \forall y : Y . \phi(x_1,y) \lor \cdots \lor \phi(x_n, y).$$
Often we can reduce the existence of the finite list $x_1, \ldots, x_n$ to a single $x$. For example, if $X$ is linearly ordered and $\phi$ is monotone in $x$ with respect to the order then we can take $x$ to be the largest one of $x_1, \ldots, x_n$.

To see how this principle is applied in a familiar case, let us look at the statement that $f : [0,1] \to \mathbb{R}$ is a continuous function. We keep $\epsilon &gt; 0$ as a free variable in order not to get confused about an outer universal quantifier:
$$\forall x \in [0,1] . \exists \delta &gt; 0 . \forall y \in [x - \delta, x + \delta] . |f(y) - f(x)| &lt; \epsilon.$$
Because $[x - \delta, x + \delta]$ is compact and comparison of reals is semidecidable, the statement $\phi(x, \delta) \equiv \forall y \in [x - \delta, x + \delta] . |f(y) - f(x)| &lt; \epsilon$ is semidecidable. The positive reals are overt and $[0,1]$ is compact, so we can apply the principle:
$$\exists \delta_1, \delta_2, \ldots, \delta_n &gt; 0 . \forall x \in [0,1] . \phi(\delta_1, x) \lor \cdots \phi(\delta_n, x).$$
Since $\phi(\delta, x)$ is antimonotone in $\delta$ the smallest one of $\delta_1, \ldots, \delta_n$ does the job already, so we just need one $\delta$:
$$\exists \delta &gt; 0 . \forall x \in [0,1] . \forall y \in [x - \delta, x + \delta] . |f(y) - f(x)| &lt; \epsilon.$$
What we have got is uniform continuity of $f$.

Vaguely speaking, a datatype is compact if it has a computable universal quantifier and overt if it has a computable existential quantifier. The (non-negative) integers $\mathbb{N}$ are overt because in order to semidecide whether $\exists n \in \mathbb{N} . \phi(n)$, with $\phi(n)$ semidecidable, we perform the paralel search by dovetailing. The Cantor space $2^\mathbb{N}$ is compact and overt, as explained by Paul Taylor's Abstract Stone Duality and Martin Escardo's "Synthetic Topology of Datatypes and Classical Spaces" (also see the related notion of searchable spaces).

Let us apply the principle to the example you mentioned. We view a language as a map from (finite) words over a fixed alphabet to boolean values. Since finite words are in computable bijective correspondence with integers we may view a language as a map from integers to boolean values. That is, the datatype of all languages is, up to computable isomorphism, precisely the Cantor space nat -&gt; bool, or in mathematical notation $2^\mathbb{N}$, which is compact. A polynomial-time Turing machine is described by its program, which is a finite string, thus the space of all (representations of) Turing machines can be taken to be nat or $\mathbb{N}$, which is overt.

Given a Turing machine $M$ and a language $c$, the statement $\mathsf{rejects}(M,c)$ which says "language $c$ is rejected by $M$" is semidecidable because it is in fact decidable: just run $M$ with input $c$ and see what it does. The conditions for our principle are satisfied! The statement "every oracle machine $M$ has a language $b$ such that $b$ is not accepted by $M^b$" is written symbolically as
$$\forall M : \mathbb{N} . \exists b : 2^\mathbb{N} . \mathsf{rejects}(M^b,b).$$
After inversion of quantifiers we get
$$\exists b_1, \ldots, b_n : 2^\mathbb{N} . \forall M : \mathbb{N} . \mathsf{rejects}(M^{b_1}, b_1) \lor \cdots \lor \mathsf{rejects}(M^{b_n},b_n).$$
Ok, so we are down to finitely many languages. Can we combine them into a single one? I will leave that as an exercise (for myself and you!).

You might also be interested in the slightly more general question of how to transform $\forall x . \exists y . \phi(x,y)$ to an equivalent statement of the form $\exists u . \forall v . \psi(u,v)$, or vice versa. There are several ways of doing this, for example:


Skolem normal form,
Herbrand normal form,
Gödel's functional interpretation.