Verify correctness of quantifier elimination, using SAT
Here are two techniques I've been able to identify:


Identify an explicit Skolem function. Suppose Priscilla can identify an explicit function $f$ such that

$$\forall x . P(x) \Leftrightarrow Q(x,f(x))$$

holds.  Then it follows that Priscilla's claim is correct.

This means that Priscilla can help us verify her claim by providing a function $f$ so that the above proposition holds.  We can confirm that the above proposition holds by testing the following formula for satisfiability:

$$\neg (P(x) \Leftrightarrow Q(x,f(x))).$$

If this formula is not satisfiable, then Priscilla's claim has been verified.

One caveat is that Priscilla needs to be able to identify a suitable function $f$.  A further caveat is that we need $f$ to be concretely representable in some concise form, say, as a polynomial-sized boolean circuit.  However, if those conditions are met, then this technique should work.
A hybrid argument.  Consider the special case of this problem, where we are quantifying over a one-bit variable (rather than a $n$-bit variable); it turns out the problem is easy to solve in this case.  This suggests that we try to chain that technique $n$ times, each time removing one more bit of $y$.  It turns out that this idea will sometimes work, but not always.

Let me explain how to verify Priscilla's claim in the case where $y=(y_1)$ is a one-bit variable.  Then $\exists y . Q(x,y)$ is equivalent to $Q(x,\text{False}) \lor Q(x,\text{True})$.  The latter formula is at most twice as large as $Q$, so still polynomial sized.  Now we can use our SAT solver to test whether $Q(x,\text{False}) \lor Q(x,\text{True})$ is equivalent to $P(x)$; the equivalence holds exactly if the following formula is not satisfiable:

$$\neg (P(x) \Leftrightarrow (Q(x,\text{False}) \lor Q(x,\text{True}))).$$

So, if we're quantifying over a single bit, this gives a way to verify that the quantifier elimination was done correctly.

To solve the original problem, apply this multiple times.  Priscilla's job will be to give us $n+1$ boolean predicates $R_0,R_1,R_2,\dots,R_n$ such that

$$R_i(x,(y_{i+1},\dots,y_n)) \equiv \exists y_1,y_2,\dots,y_i . Q(x,y).$$

Our task will be to verify whether all of these boolean predicates were correctly generated.  We can do this by testing whether $Q(x,y) \equiv R_0(x,y)$, $P(x) \equiv R_n(x)$,

$$R_{i+1}(x,(y_{i+2},\dots,y_n)) \equiv \exists y_{i+1} . R_i(x,(y_{i+1},\dots,y_n)) \qquad \text{for $i=1,2,\dots,n-1$}.$$

Notice that the latter is an instance of quantifier elimination with a single bit, so we've already described how to test it was done correctly using a SAT solver.  We can also test whether $Q \equiv R_0$ and $P \equiv R$ using a SAT solver straightforwardly.  So, we can check whether Priscilla generated $R_0,\dots,R_n$ correctly.  If she did, then we've verified that $P$ was generated suitably.

One caveat is that Priscilla needs to be able to generate the $R_i$'s.  A bigger caveat is that the size of all the $R_i$'s needs to be reasonable (say, polynomial-sized).  If Priscilla generates the $R_i$'s naively, their size might grow exponentially with $i$, which is no good.  So, Priscilla will need a way to simplify at each stage; there needs to exist some sequence of $R_0,\dots,R_n$ that are all polynomial-sized, and Priscilla needs to be able to find such a sequence.  That is by no means guaranteed.  That said, if Priscilla can do this, then this technique should work.


I'm not fully satisfied with these techniques -- they are incomplete heuristics, and they might fail on some/many problem instances -- so I would still be interested to see other ways of approaching this problem.