<p>To me, the "canonical" proof of the Karp-Lipton theorem (that $NP \subseteq P/poly \Longrightarrow \Pi_2 P = \Sigma_2 P$) has this flavor. But here it is not the actual theorem statement in which quantifiers get reversed, but rather the "quantifiers" get reversed within the model of alternating computation, using the assumption that $NP$ has small circuits. </p>

<p>You want to simulate a computation of the form </p>

<p>$(\forall y)(\exists z)R(x,y,z)$ </p>

<p>where $R$ is a polynomial-time predicate. You can do this by guessing a small circuit $C$ for (say) satisfiability, modifying $C$ so that it checks itself and produces a satisfying assignment when its input is satisfiable. Then for all $y$, create a SAT instance $S(x,y)$ that's equivalent to $(\exists z)R(x,y,z)$ and solve it. So you've produced an equivalent computation of the form</p>

<p>$(\exists C)(\forall y)[S(x,y)$ is satisfiable according to $C]$.</p>

CC BY-SA 2.5
2011-01-22T19:43:34.877Z
Outstanding! This is an example of assumption-based quantifier switching.
Sadeq Dousti
CC BY-SA 2.5
2011-01-23T10:18:41.647Z
Although this is perfectly correct, I wanted to suggest writing $NP \subset P/poly$ instead of $NP \subseteq P/poly$, since NP can never equal P/poly.
Sadeq Dousti
CC BY-SA 2.5
2011-01-22T19:18:03.823Z
2011-01-22T19:18:03.823Z
Ryan Williams
<p>Impagliazzo's hard-core set lemma allows you to switch quantifiers in the context of computational-hardness assumptions. Here's the <a href="http://cseweb.ucsd.edu/~russell/hardcore.ps">original paper</a>. You can find tons of related papers and posts by Googling.</p>

<p>The lemma says that if <em>for every</em> algorithm A <em>there exists</em> a large set of inputs on which A fails to compute a fixed function f, then in fact <em>there exists</em> a large set of inputs on which <em>every</em> algorithm fails to compute f with probability close to 1/2.</p>

<p>This lemma can be proved using the min-max theorem or boosting (a technique from computational learning theory), both of which are examples of switching quantifiers.</p>

CC BY-SA 2.5
2011-01-22T17:16:11.563Z
That's an excellent point.
Suresh Venkat
CC BY-SA 2.5
2011-01-22T14:41:48.933Z
2011-01-22T14:41:48.933Z
Manu
<p>The basic use of union bound in the probabilistic method can be interpreted as a way to reverse the order of quantifiers.  Although this is already mentioned in the question implicitly because the proof by Impagliazzo and Rudich is an example of this, I think that it is worth stating more explicitly.</p>

<p>Suppose that <i>X</i> is finite and that for every <i>x</i>∈<i>X</i>, we know not only that some <i>y</i>∈<i>Y</i> satisfies <i>φ</i>(<i>x</i>,<i>y</i>) but also that many choices of <i>y</i>∈<i>Y</i> satisfy <i>φ</i>(<i>x</i>,<i>y</i>).  Formally, suppose that we know (∀<i>x</i>∈<i>X</i>) Pr<sub><i>y</i>∈<i>Y</i></sub> [￢<i>φ</i>(<i>x</i>,<i>y</i>)] &lt; 1/|<i>X</i>| for some probabilistic measure on <i>Y</i>.  Then union bound allows us to conclude Pr<sub><i>y</i>∈<i>Y</i></sub> [(∃<i>x</i>∈<i>X</i>) ￢<i>φ</i>(<i>x</i>,<i>y</i>)] &lt; 1, which is equivalent to (∃<i>y</i>∈<i>Y</i>) (∀<i>x</i>∈<i>X</i>) <i>φ</i>(<i>x</i>,<i>y</i>).</p>

<p>There are variations of this argument:</p>

<ol>
<li><p>If <i>X</i> is infinite, we can sometimes discretize <i>X</i> by considering a suitable metric on <i>X</i> and an <i>ε</i>-net of it.  After discretizing <i>X</i>, we can use union bound as above.</p></li>
<li><p>When the events <i>φ</i>(<i>x</i>,<i>y</i>) for different values of <i>x</i> are almost independent, we can use the <a href="http://en.wikipedia.org/wiki/Lov%C3%A1sz_local_lemma">Lovász local lemma</a> instead of union bound.</p></li>
</ol>

CC BY-SA 2.5
2011-01-25T00:39:56.783Z
Tsuyoshi, this is terribly off topic, but it's time to nominate yourself as a moderator :)
Suresh Venkat
CC BY-SA 2.5
2011-01-24T12:25:09.310Z
2011-01-24T12:25:09.310Z
Tsuyoshi Ito
<p>I'd like to add several other techniques. Although the first two techniques are <strong>not</strong> exactly for reversing the order of universal and existential quantifiers, they have a very similar flavor. Therefore, I took the opportunity to describe them here:</p>
<blockquote>
<p><strong>Averaging Lemma:</strong> Used to prove <span class="math-container">$BPP \subset P/poly$</span> and many other interesting theorems. <em>Informally</em>, assume that <span class="math-container">$S$</span> denotes the set of subscribers to some library, <span class="math-container">$B$</span> denotes the set of books in the library, and for <span class="math-container">$s\in S$</span> and <span class="math-container">$b \in B$</span>, the proposition <span class="math-container">$\phi(s,b)$</span> is true iff &quot;subscriber <span class="math-container">$s$</span> likes the book <span class="math-container">$b$</span>.&quot; The averaging lemma states that: if for every <span class="math-container">$s \in S$</span>, there exists at least 2/3 of <span class="math-container">$b$</span>'s in <span class="math-container">$B$</span> such that <span class="math-container">$\phi(s,b)$</span> holds, then there exists a single <span class="math-container">$b \in B$</span>, such that for at least 2/3 of <span class="math-container">$s$</span>'s in <span class="math-container">$S$</span>, the proposition <span class="math-container">$\phi(s,b)$</span> holds. (This can be easily proven via <em>reductio ad absurdum</em> and a counting argument.)</p>
</blockquote>
<p>Now let <span class="math-container">$L \in BPP$</span>, and let <span class="math-container">$M(\cdot)$</span> be a PPT machine which decides <span class="math-container">$L$</span>. Suppose that the running time of <span class="math-container">$M$</span> is bounded by a polynomial <span class="math-container">$q(\cdot)$</span>. Then, for any <span class="math-container">$x \in \{0,1\}^*$</span>, and for at least 2/3 of <span class="math-container">$r$</span>'s, <span class="math-container">$r \in \{0,1\}^{q(|x|)}$</span>, it holds that <span class="math-container">$M_r(x) = \chi_L(x)$</span>. Here, <span class="math-container">$M_r(\cdot)$</span> is the machine <span class="math-container">$M$</span> which uses randomness <span class="math-container">$r$</span>, and <span class="math-container">$\chi_L(\cdot)$</span> is the characteristic function of <span class="math-container">$L$</span>. The averaging lemma is then used to show that for any <span class="math-container">$n \in \mathbb{N}$</span>, there exists a single <span class="math-container">$r \in \{0,1\}^{q(n)}$</span>, such that for at least 2/3 of <span class="math-container">$x$</span>'s of length <span class="math-container">$n$</span>, <span class="math-container">$M_r(x) = \chi_L(x)$</span>. This single <span class="math-container">$r$</span> works as an advice to <span class="math-container">$M$</span>, and therefore <span class="math-container">$BPP \subset P/poly$</span>.</p>
<p><code>NOTE: I re-emphasize that this is not a quantifier switching technique, but it has the same spirit.</code></p>
<blockquote>
<p><strong>Swapping Lemma:</strong> <a href="http://www.springerlink.com/content/pk10854562152285/" rel="noreferrer">Zachos and Fürer</a> introduced a new <em>probabilistic</em> quantifier <span class="math-container">$\exists^+$</span> (which roughly means &quot;for most&quot;). They proved that (omitting details):</p>
<p><span class="math-container">$(\forall y)(\exists^+z) \phi(x,y,z) \Rightarrow (\exists^+ \mathbf{C})(\forall y)(\exists z \in \mathbf{C})\phi(x,y,z)$</span></p>
<p>Note that this is a second-order logic theorem.</p>
</blockquote>
<p>Using the swapping lemma, they proved a number of interesting theorems, such as the BPP-theorem and Babai's <span class="math-container">$MA \subseteq AM$</span> theorem. I refer you to the original paper for more information.</p>
<blockquote>
<p>A theorem similar to Karp-Lipton theorem mentioned in <a href="https://cstheory.stackexchange.com/questions/4473/techniques-for-reversing-the-order-of-quantiers/4484#4484">Ryan Williams</a> post: <span class="math-container">$coNP \subset NP/Poly \Longrightarrow \Pi_3 P = \Sigma_3 P$</span>.</p>
</blockquote>

CC BY-SA 2.5
2011-01-25T20:58:26.667Z
Nitpicking: I would like to note that the actual proof of BPP⊆P/poly requires a little more than what is written here, because an advice string which works only for 2/3 fraction of instances is insufficient.  But I think that the important point of the first half of this answer is that the proof of BPP⊆P/poly can be viewed as something similar to quantifier reversal, which is perfectly valid.
Tsuyoshi Ito
CC BY-SA 2.5
2011-01-25T23:30:59.793Z
@Tsuyoshi: You are right. But the rest of proof uses the sequential repetition and Chernoff bound, to prove the existence of an $r$ which works for all but an exponentially small fraction of inputs; and as you said, that does not have to do with quantifier reversal, so I omitted it.
Sadeq Dousti
CC BY-SA 2.5
2011-01-26T01:00:42.993Z
I am not sure if you got my point.  My point is that the statement of the “averaging lemma” is not sufficient to prove BPP⊆P/poly.  You need a slightly finer estimate, namely the estimate of the expected probability E_b [Pr_s φ(s,b)] instead of max_b [Pr_s φ(s,b)].
Tsuyoshi Ito
CC BY-SA 2.5
2011-01-26T08:16:57.860Z
@Tsuyoshi: I'm afraid I didn't get you. In the previous comment, I noted that we first amplify the 1/3 error to $2^{-|x|}$, and then apply the averaging lemma. [Here](http://s1.bild.me/bilder/311010/8971737AveragingLemma.PNG) is a full-blown proof, taken from Goldreich's book. Am I missing something?
Sadeq Dousti
CC BY-SA 2.5
2011-01-26T21:03:45.987Z
Thanks!  I had been misunderstanding your comment.  I did not know that BPP⊆P/poly can be proved by first reducing the error and then applying the averaging lemma (I was thinking of the opposite order).
Tsuyoshi Ito
CC BY-SA 2.5
2011-01-27T03:36:24.520Z
@Tsuyoshi: You're most welcome!
Sadeq Dousti
CC BY-SA 2.5
2011-01-23T10:14:40.000Z
2011-01-23T10:14:40.000Z
2020-06-17T09:38:08.363Z
Sadeq Dousti
<p>Reversal of quantifiers is an important property that is often behind well known theorems.</p>

<p>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 <em>pointwise</em> and <em>uniform</em> continuity. A well known theorem says that every pointwise continuous map is uniformly continuous, provided the domain is nice, i.e., <em>compact</em>.</p>

<p>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$.</p>

<p>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 <em>uniform</em> continuity of $f$.</p>

<p>Vaguely speaking, a datatype is <em>compact</em> if it has a computable universal quantifier and <em>overt</em> 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 <a href="http://en.wikipedia.org/wiki/Dovetailing_%28computer_science%29">dovetailing</a>. The Cantor space $2^\mathbb{N}$ is compact and overt, as explained by Paul Taylor's <a href="http://www.paultaylor.eu/ASD/">Abstract Stone Duality</a> and Martin Escardo's "<a href="http://www.cs.bham.ac.uk/~mhe/papers/entcs87.pdf">Synthetic Topology of Datatypes and Classical Spaces</a>" (also see the related notion of <a href="http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/">searchable spaces</a>).</p>

<p>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 <code>nat -&gt; bool</code>, 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 <code>nat</code> or $\mathbb{N}$, which is overt.</p>

<p>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!).</p>

<p>You might also be interested in the slightly more general question of how to <em>transform</em> $\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:</p>

<ul>
<li><a href="http://en.wikipedia.org/wiki/Skolem_normal_form">Skolem normal form</a>,</li>
<li><a href="http://en.wikipedia.org/wiki/Herbrand_normal_form">Herbrand normal form</a>,</li>
<li><a href="http://en.wikipedia.org/wiki/Dialectica_interpretation">Gödel's functional interpretation</a>.</li>
</ul>

CC BY-SA 2.5
2011-01-22T10:50:08.937Z
Very nice. I must admit that my knowledge is challenged by your answer, and I have to read it several times to grasp. (I just finished pass 1!) I think you have answered another important question I had in mind, too: **What are the necessary and/or sufficient conditions for quantifier switching?** Am I right?
Sadeq Dousti
CC BY-SA 2.5
2011-01-22T10:51:20.107Z
And another quick question: Does you answer imply **techniques**, or just the conditions?
Sadeq Dousti
CC BY-SA 2.5
2011-01-22T13:08:20.637Z
It is a very general condition (one space must be overt, the other compact, and the relation open), but it is also a technique: if you can find topologies that satisfy the conditions then you can invert the quantifiers.
Andrej Bauer
CC BY-SA 2.5
2011-01-22T16:28:10.527Z
@Andrej, your answer is *really* good and educational. I never knew there's a relation between compactness and reversing quantifiers, until this post appears. I feel enlightened.
Hsien-Chih Chang 張顯之
CC BY-SA 2.5
2011-01-22T17:14:54.777Z
What an amazing answer.
Suresh Venkat
CC BY-SA 2.5
2011-01-22T17:21:59.320Z
I feel flattered. I wish more people knew about the intimate connections between logic, computation and topology.
Andrej Bauer
CC BY-SA 2.5
2011-01-22T19:55:03.860Z
@Andrej: Is there a good reference (specially a book or a lecture note) on the "intimate connections between logic, computation and topology"?
Sadeq Dousti
CC BY-SA 2.5
2011-01-22T21:03:57.320Z
Great Answer Andrej...I feel that my neurons are jumping. A very big thanks!
Akash Kumar
CC BY-SA 2.5
2011-01-22T22:46:33.283Z
@Andrej: Started reading with tea. Had to take a break and come back with coffee. ;) I love it, great answer!
Daniel Apon
CC BY-SA 2.5
2011-01-22T23:02:14.207Z
@Andrej, maybe you should write something on your blog.
Suresh Venkat
CC BY-SA 2.5
2011-01-23T01:07:15.127Z
@Sadeq I'm not sure if this is what Andrej is talking about, but there's "Physics, Topology, Logic and Computation: A Rosetta Stone" by Baez and Stay. It's a short manuscript that's easily found on Google.
Mark Reitblatt
CC BY-SA 2.5
2011-01-23T06:14:04.643Z
@Mark: Seems like a promising source of study. There are even slides available, which makes reading easier. I'm still eager to know what's behind @Andrej's magical answer :D
Sadeq Dousti
CC BY-SA 2.5
2011-01-23T17:35:40.113Z
@Sadeq: Follow the links in his post. Both Taylor and Escardo have poured shocking amounts of effort into exposition. Also, you might enjoy Steve Vickers' *Topology via Logic*. (I was somewhat disappointed by the Baez and Stay paper because IMO they presented linear logic in an unnecessarily confusing way.)
Neel Krishnaswami
CC BY-SA 2.5
2011-01-24T20:23:00.233Z
@Sadeq: there is now a regular conference called Topology, Algebra, and Categories in Logic which explores these intimate connections: http://www.lif.univ-mrs.fr/~lsantoca/tacl2011/
András Salamon
CC BY-SA 2.5
2011-02-02T13:08:14.853Z
A quibble: your last point talks of transformations of formulae into "equivalent" formulae: this is sloppy language, I think.  Skolem/Herbrandisation conserves provability, but you can usually find intepretations that distinguish them, while the equivalence of the two formulae in the Dialectica interpretation need not be constructively valid.  It's worth talking in the more careful terms of "conserves soundness/provability", I think.
Charles Stewart
CC BY-SA 2.5
2011-02-02T20:03:39.150Z
@Charles: I agree with you in principle, and that is how I would talk if I talked to logicians.
Andrej Bauer
CC BY-SA 2.5
2011-02-02T20:13:40.837Z
@Andrej: I am the sloppy one - Skolem/Herbrandisation conserves satisfiability, which is the dual of conserving provability.  I seem to recall there being a moral truth about all quibbles containing errors.
Charles Stewart
CC BY-SA 2.5
2011-01-22T09:30:09.927Z
2011-01-22T17:17:14.850Z
2011-01-22T17:17:14.850Z
Andrej Bauer
<p>It is well-known that in general, the order of universal and existential quantifiers cannot be reversed. In other words, for a general logical formula $\phi(\cdot,\cdot)$,</p>

<p>$(\forall x)(\exists y) \phi(x,y) \quad \not\Leftrightarrow \quad (\exists y)(\forall x) \phi(x,y)$</p>

<p>On the other hand, we know the right-hand side is more restrictive than the left-hand side; that is, $(\exists y)(\forall x) \phi(x,y) \Rightarrow (\forall x)(\exists y) \phi(x,y)$. </p>

<p>This question focuses on techniques to derive $(\forall x)(\exists y) \phi(x,y) \Rightarrow (\exists y)(\forall x) \phi(x,y)$, whenever it holds for $\phi(\cdot,\cdot)$.</p>

<p><strong>Diagonalization</strong> is one such technique. I first see this use of diagonalization in the paper <a href="http://dx.doi.org/10.1137/0204037">Relativizations of the $\mathcal{P} \overset{?}{=} \mathcal{NP}$ Question</a> (see also the <a href="http://www.cs.umd.edu/~jkatz/complexity/relativization.pdf">short note by Katz</a>). In that paper, the authors first prove that:</p>

<blockquote>
  <p>For any deterministic, polynomial-time oracle machine M, there exists a language B such that $L_B \ne L(M^B)$.</p>
</blockquote>

<p>They then reverse the order of the quantifiers (using <strong>diagonalization</strong>), to prove that:</p>

<blockquote>
  <p>There exists a language B such that for all deterministic, poly-time M we have $L_B \ne L(M^B)$.</p>
</blockquote>

<p>This technique is used in other papers, such as <a href="http://eprint.iacr.org/1998/011.pdf">[CGH]</a> and <a href="http://linkinghub.elsevier.com/retrieve/pii/089054019190024V">[AH]</a>.</p>

<p>I found another technique in the proof of Theorem 6.3 of <a href="http://portal.acm.org/citation.cfm?id=73007.73012">[IR]</a>. It uses a combination of <strong>measure theory</strong> and <strong>pigeon-hole principle</strong> to reverse the order of quantifiers.</p>

<blockquote>
  <p>I want to know what other techniques are used in computer science, to reverse the order of universal and existential quantifiers?</p>
</blockquote>

CC BY-SA 2.5
2011-01-22T02:17:03.713Z
Wow, this is a great question. Just reading it made me look at "familiar" objects differently. Thanks!
Mark Reitblatt
<lo.logic><big-picture><proof-techniques>
Techniques for Reversing the Order of Quantiﬁers
Sadeq Dousti
# Techniques for Reversing the Order of Quantiﬁers

(Asked by: username_0 on 2011-01-21)

It is well-known that in general, the order of universal and existential quantifiers cannot be reversed. In other words, for a general logical formula $\phi(\cdot,\cdot)$,

$(\forall x)(\exists y) \phi(x,y) \quad \not\Leftrightarrow \quad (\exists y)(\forall x) \phi(x,y)$

On the other hand, we know the right-hand side is more restrictive than the left-hand side; that is, $(\exists y)(\forall x) \phi(x,y) \Rightarrow (\forall x)(\exists y) \phi(x,y)$.

This question focuses on techniques to derive $(\forall x)(\exists y) \phi(x,y) \Rightarrow (\exists y)(\forall x) \phi(x,y)$, whenever it holds for $\phi(\cdot,\cdot)$.

**Diagonalization** is one such technique. I first see this use of diagonalization in the paper [Relativizations of the $\mathcal{P} \overset{?}{=} \mathcal{NP}$ Question](http://dx.doi.org/10.1137/0204037) (see also the [short note by Katz](http://www.cs.umd.edu/~jkatz/complexity/relativization.pdf)). In that paper, the authors first prove that:

> For any deterministic, polynomial-time oracle machine M, there exists a language B such that $L\_B \ne L(M^B)$.

They then reverse the order of the quantifiers (using **diagonalization**), to prove that:

> There exists a language B such that for all deterministic, poly-time M we have $L\_B \ne L(M^B)$.

This technique is used in other papers, such as [[CGH]](http://eprint.iacr.org/1998/011.pdf) and [[AH]](http://linkinghub.elsevier.com/retrieve/pii/089054019190024V).

I found another technique in the proof of Theorem 6.3 of [[IR]](http://portal.acm.org/citation.cfm?id=73007.73012). It uses a combination of **measure theory** and **pigeon-hole principle** to reverse the order of quantifiers.

> I want to know what other techniques are used in computer science, to reverse the order of universal and existential quantifiers?

**Tags:** lo.logic, big-picture, proof-techniques

> **Comments:**
> **username_1**: Wow, this is a great question. Just reading it made me look at "familiar" objects differently. Thanks!  

---

## 5 answers

### Answer by username_6 on 2011-01-22. Score: 80 | Accepted answer

Reversal of quantifiers is an important property that is often behind well known theorems.

For example, in analysis the difference between $\forall \epsilon > 0 . \forall x . \exists \delta > 0$ and $\forall \epsilon > 0 . \exists \delta > 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 > 0$ as a free variable in order not to get confused about an outer universal quantifier:
$$\forall x \in [0,1] . \exists \delta > 0 . \forall y \in [x - \delta, x + \delta] . |f(y) - f(x)| < \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)| < \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 > 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 > 0 . \forall x \in [0,1] . \forall y \in [x - \delta, x + \delta] . |f(y) - f(x)| < \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](http://en.wikipedia.org/wiki/Dovetailing_%28computer_science%29). The Cantor space $2^\mathbb{N}$ is compact and overt, as explained by Paul Taylor's [Abstract Stone Duality](http://www.paultaylor.eu/ASD/) and Martin Escardo's "[Synthetic Topology of Datatypes and Classical Spaces](http://www.cs.bham.ac.uk/~mhe/papers/entcs87.pdf)" (also see the related notion of [searchable spaces](http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/)).

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 -> 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](http://en.wikipedia.org/wiki/Skolem_normal_form),
* [Herbrand normal form](http://en.wikipedia.org/wiki/Herbrand_normal_form),
* [Gödel's functional interpretation](http://en.wikipedia.org/wiki/Dialectica_interpretation).

> **Comments:**
> **username_0**: Very nice. I must admit that my knowledge is challenged by your answer, and I have to read it several times to grasp. (I just finished pass 1!) I think you have answered another important question I had in mind, too: **What are the necessary and/or sufficient conditions for quantifier switching?** Am I right?  
> **username_0**: And another quick question: Does you answer imply **techniques**, or just the conditions?  
> **username_6**: It is a very general condition (one space must be overt, the other compact, and the relation open), but it is also a technique: if you can find topologies that satisfy the conditions then you can invert the quantifiers.  
> **username_7**: @Andrej, your answer is *really* good and educational. I never knew there's a relation between compactness and reversing quantifiers, until this post appears. I feel enlightened.  
> **username_4**: What an amazing answer.  
> **username_6**: I feel flattered. I wish more people knew about the intimate connections between logic, computation and topology.  
> **username_0**: @Andrej: Is there a good reference (specially a book or a lecture note) on the "intimate connections between logic, computation and topology"?  
> **username_8**: Great Answer Andrej...I feel that my neurons are jumping. A very big thanks!  
> **username_9**: @Andrej: Started reading with tea. Had to take a break and come back with coffee. ;) I love it, great answer!  
> **username_4**: @Andrej, maybe you should write something on your blog.  
> **username_1**: @Sadeq I'm not sure if this is what Andrej is talking about, but there's "Physics, Topology, Logic and Computation: A Rosetta Stone" by Baez and Stay. It's a short manuscript that's easily found on Google.  
> **username_0**: @Mark: Seems like a promising source of study. There are even slides available, which makes reading easier. I'm still eager to know what's behind @Andrej's magical answer :D  
> **username_10**: @Sadeq: Follow the links in his post. Both Taylor and Escardo have poured shocking amounts of effort into exposition. Also, you might enjoy Steve Vickers' *Topology via Logic*. (I was somewhat disappointed by the Baez and Stay paper because IMO they presented linear logic in an unnecessarily confusing way.)  
> **username_11**: @Sadeq: there is now a regular conference called Topology, Algebra, and Categories in Logic which explores these intimate connections: http://www.lif.univ-mrs.fr/~lsantoca/tacl2011/  
> **username_12**: A quibble: your last point talks of transformations of formulae into "equivalent" formulae: this is sloppy language, I think.  Skolem/Herbrandisation conserves provability, but you can usually find intepretations that distinguish them, while the equivalence of the two formulae in the Dialectica interpretation need not be constructively valid.  It's worth talking in the more careful terms of "conserves soundness/provability", I think.  
> **username_6**: @Charles: I agree with you in principle, and that is how I would talk if I talked to logicians.  
> **username_12**: @Andrej: I am the sloppy one - Skolem/Herbrandisation conserves satisfiability, which is the dual of conserving provability.  I seem to recall there being a moral truth about all quibbles containing errors.  

---

### Answer by username_3 on 2011-01-22. Score: 26

Impagliazzo's hard-core set lemma allows you to switch quantifiers in the context of computational-hardness assumptions. Here's the [original paper](http://cseweb.ucsd.edu/~russell/hardcore.ps). You can find tons of related papers and posts by Googling.

The lemma says that if *for every* algorithm A *there exists* a large set of inputs on which A fails to compute a fixed function f, then in fact *there exists* a large set of inputs on which *every* algorithm fails to compute f with probability close to 1/2.

This lemma can be proved using the min-max theorem or boosting (a technique from computational learning theory), both of which are examples of switching quantifiers.

> **Comments:**
> **username_4**: That's an excellent point.  

---

### Answer by username_2 on 2011-01-22. Score: 17

To me, the "canonical" proof of the Karp-Lipton theorem (that $NP \subseteq P/poly \Longrightarrow \Pi\_2 P = \Sigma\_2 P$) has this flavor. But here it is not the actual theorem statement in which quantifiers get reversed, but rather the "quantifiers" get reversed within the model of alternating computation, using the assumption that $NP$ has small circuits.

You want to simulate a computation of the form

$(\forall y)(\exists z)R(x,y,z)$

where $R$ is a polynomial-time predicate. You can do this by guessing a small circuit $C$ for (say) satisfiability, modifying $C$ so that it checks itself and produces a satisfying assignment when its input is satisfiable. Then for all $y$, create a SAT instance $S(x,y)$ that's equivalent to $(\exists z)R(x,y,z)$ and solve it. So you've produced an equivalent computation of the form

$(\exists C)(\forall y)[S(x,y)$ is satisfiable according to $C]$.

> **Comments:**
> **username_0**: Outstanding! This is an example of assumption-based quantifier switching.  
> **username_0**: Although this is perfectly correct, I wanted to suggest writing $NP \subset P/poly$ instead of $NP \subseteq P/poly$, since NP can never equal P/poly.  

---

### Answer by username_5 on 2011-01-24. Score: 12

The basic use of union bound in the probabilistic method can be interpreted as a way to reverse the order of quantifiers. Although this is already mentioned in the question implicitly because the proof by Impagliazzo and Rudich is an example of this, I think that it is worth stating more explicitly.

Suppose that *X* is finite and that for every *x*∈*X*, we know not only that some *y*∈*Y* satisfies *φ*(*x*,*y*) but also that many choices of *y*∈*Y* satisfy *φ*(*x*,*y*). Formally, suppose that we know (∀*x*∈*X*) Pr*y*∈*Y* [￢*φ*(*x*,*y*)] < 1/|*X*| for some probabilistic measure on *Y*. Then union bound allows us to conclude Pr*y*∈*Y* [(∃*x*∈*X*) ￢*φ*(*x*,*y*)] < 1, which is equivalent to (∃*y*∈*Y*) (∀*x*∈*X*) *φ*(*x*,*y*).

There are variations of this argument:

1. If *X* is infinite, we can sometimes discretize *X* by considering a suitable metric on *X* and an *ε*-net of it. After discretizing *X*, we can use union bound as above.
2. When the events *φ*(*x*,*y*) for different values of *x* are almost independent, we can use the [Lovász local lemma](http://en.wikipedia.org/wiki/Lov%C3%A1sz_local_lemma) instead of union bound.

> **Comments:**
> **username_4**: Tsuyoshi, this is terribly off topic, but it's time to nominate yourself as a moderator :)  

---

### Answer by username_0 on 2011-01-23. Score: 10

I'd like to add several other techniques. Although the first two techniques are **not** exactly for reversing the order of universal and existential quantifiers, they have a very similar flavor. Therefore, I took the opportunity to describe them here:

> **Averaging Lemma:** Used to prove $BPP \subset P/poly$ and many other interesting theorems. *Informally*, assume that $S$ denotes the set of subscribers to some library, $B$ denotes the set of books in the library, and for $s\in S$ and $b \in B$, the proposition $\phi(s,b)$ is true iff "subscriber $s$ likes the book $b$." The averaging lemma states that: if for every $s \in S$, there exists at least 2/3 of $b$'s in $B$ such that $\phi(s,b)$ holds, then there exists a single $b \in B$, such that for at least 2/3 of $s$'s in $S$, the proposition $\phi(s,b)$ holds. (This can be easily proven via *reductio ad absurdum* and a counting argument.)

Now let $L \in BPP$, and let $M(\cdot)$ be a PPT machine which decides $L$. Suppose that the running time of $M$ is bounded by a polynomial $q(\cdot)$. Then, for any $x \in \{0,1\}^\*$, and for at least 2/3 of $r$'s, $r \in \{0,1\}^{q(|x|)}$, it holds that $M\_r(x) = \chi\_L(x)$. Here, $M\_r(\cdot)$ is the machine $M$ which uses randomness $r$, and $\chi\_L(\cdot)$ is the characteristic function of $L$. The averaging lemma is then used to show that for any $n \in \mathbb{N}$, there exists a single $r \in \{0,1\}^{q(n)}$, such that for at least 2/3 of $x$'s of length $n$, $M\_r(x) = \chi\_L(x)$. This single $r$ works as an advice to $M$, and therefore $BPP \subset P/poly$.

`NOTE: I re-emphasize that this is not a quantifier switching technique, but it has the same spirit.`

> **Swapping Lemma:** [Zachos and Fürer](http://www.springerlink.com/content/pk10854562152285/) introduced a new *probabilistic* quantifier $\exists^+$ (which roughly means "for most"). They proved that (omitting details):
>
> $(\forall y)(\exists^+z) \phi(x,y,z) \Rightarrow (\exists^+ \mathbf{C})(\forall y)(\exists z \in \mathbf{C})\phi(x,y,z)$
>
> Note that this is a second-order logic theorem.

Using the swapping lemma, they proved a number of interesting theorems, such as the BPP-theorem and Babai's $MA \subseteq AM$ theorem. I refer you to the original paper for more information.

> A theorem similar to Karp-Lipton theorem mentioned in [username_2](https://cstheory.stackexchange.com/questions/4473/techniques-for-reversing-the-order-of-quantiers/4484#4484) post: $coNP \subset NP/Poly \Longrightarrow \Pi\_3 P = \Sigma\_3 P$.

> **Comments:**
> **username_5**: Nitpicking: I would like to note that the actual proof of BPP⊆P/poly requires a little more than what is written here, because an advice string which works only for 2/3 fraction of instances is insufficient.  But I think that the important point of the first half of this answer is that the proof of BPP⊆P/poly can be viewed as something similar to quantifier reversal, which is perfectly valid.  
> **username_0**: @Tsuyoshi: You are right. But the rest of proof uses the sequential repetition and Chernoff bound, to prove the existence of an $r$ which works for all but an exponentially small fraction of inputs; and as you said, that does not have to do with quantifier reversal, so I omitted it.  
> **username_5**: I am not sure if you got my point.  My point is that the statement of the “averaging lemma” is not sufficient to prove BPP⊆P/poly.  You need a slightly finer estimate, namely the estimate of the expected probability E_b [Pr_s φ(s,b)] instead of max_b [Pr_s φ(s,b)].  
> **username_0**: @Tsuyoshi: I'm afraid I didn't get you. In the previous comment, I noted that we first amplify the 1/3 error to $2^{-|x|}$, and then apply the averaging lemma. [Here](http://s1.bild.me/bilder/311010/8971737AveragingLemma.PNG) is a full-blown proof, taken from Goldreich's book. Am I missing something?  
> **username_5**: Thanks!  I had been misunderstanding your comment.  I did not know that BPP⊆P/poly can be proved by first reducing the error and then applying the averaging lemma (I was thinking of the opposite order).  
> **username_0**: @Tsuyoshi: You're most welcome!  

---

