Buggy Reduce/Resolve function?

Question

It seems to me that this is a clear-cut case of Mathematica actually producing the wrong answer (with no warnings).

I'm trying to express the fact that for any integer, there exists a factorization (even if that factorization is just n = n * 1). But Mathematica says no.

If I replace the domain with Reals or Complexes, then it says True.

Is this a bug or am I using these functions incorrectly?

Resolve[ForAll[n, Exists[{p, q}, p*q == n]], Integers]

(*Out[1]= False*)

Reduce[ForAll[n, Exists[{p, q}, p*q == n]], {n, p, q}, Integers]

(*Out[2]= False*)

Answer 1

I think it is a limitation of Resolve[].

As stated in the help:

Resolve[expr] can in principle always eliminate quantifiers if expr contains only polynomial equations and inequalities over the reals or complexes.

It shouldn't return False, though.

Edit

I am sure this

Trace[Resolve[ForAll[n, Exists[{p, q}, p q == n]], Integers], TraceInternal -> True]

must explain what is happening ... but I wrote the relevant notes in the margin of some notebook and I can't find them now :)