# Buggy Reduce/Resolve function?

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*)

-
FullSimplify[ForAll[n, Exists[{p, q}, p*q == n]], {n, p, q} \[Element] Integers] works nicely, though. – J. M. Jul 22 '12 at 19:05
@J.M. Try FullSimplify[ ForAll[n, Exists[{p, q}, p/Pi q/Sqrt@2 == n]], {n, p, q} \[Element] Integers] – Dr. belisarius Jul 22 '12 at 19:16
@bel, now that sure is nasty... – J. M. Jul 22 '12 at 19:18
@J.M. I believe the quantifiers are isolating its variables, so they are not visible to FullSimply's assumptions – Dr. belisarius Jul 22 '12 at 19:21
It doesn't seem a problem of FullSimplify, but rather of Exists/ForAll. E.g. Resolve[ForAll[n, Exists[{p, q}, p*q == n]], {n, p, q} \[Element] Integers] returns True. – Artes Jul 22 '12 at 19:34

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 :)

-