Strange result of Reduce and ForAll

Question

Bug introduced in 9.0 or earlier, present in 10.0, not present in 10.3

---

In the question Can Mathematica tell me if a polynomial has all real roots?, quite a few of interesting answers were given. I wanted to add another one, using quantors, and observed some strange results.

The polynomial $x^3-1$ has two non-real roots. So the following is as expected:

Reduce[Exists[x, x^3 == 1, Not[x ∈ Reals]]]  

(* True *)

However:

Reduce[ForAll[x, x^3 == 1, x ∈ Reals]]

(* During evaluation of In[2]:= Reduce::nsmet: This system cannot be solved with the methods available to Reduce. >> *)

The following results show that the problem has to do with the third argument in ForAll.

This works:

Reduce[ForAll[x, x == 1, x > 0] ]

(* True *)

But this does not:

Reduce[ForAll[x, x == 1, x ∈ Reals] ]

(* During evaluation of In[4]:= Reduce::nsmet: This system cannot be solved with the methods available to Reduce. >> *)

I am inclined to consider this as a bug.

Answer 1

I also think this is a bug, but at least there is a way out:

realQ[x_] := Im@x == 0 && (Re@x >= 0 || Re@x < 0) (*or just Im@x == 0 
                                                    if you aren't suspicious *)

{Reduce[Exists[x, x^3 == 1, Not[realQ@x]]],
 Reduce[ForAll[x, x^3 == 1, realQ@x]],
 Reduce[ForAll[x, x == 1, realQ@x]]}

(* {True, False, True} *)