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*)
  • $\begingroup$ FullSimplify[ForAll[n, Exists[{p, q}, p*q == n]], {n, p, q} \[Element] Integers] works nicely, though. $\endgroup$ – J. M.'s technical difficulties Jul 22 '12 at 19:05
  • $\begingroup$ @J.M. Try FullSimplify[ ForAll[n, Exists[{p, q}, p/Pi q/Sqrt@2 == n]], {n, p, q} \[Element] Integers] $\endgroup$ – Dr. belisarius Jul 22 '12 at 19:16
  • $\begingroup$ @bel, now that sure is nasty... $\endgroup$ – J. M.'s technical difficulties Jul 22 '12 at 19:18
  • $\begingroup$ @J.M. I believe the quantifiers are isolating its variables, so they are not visible to FullSimply's assumptions $\endgroup$ – Dr. belisarius Jul 22 '12 at 19:21
  • $\begingroup$ 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. $\endgroup$ – 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.


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

|improve this answer|||||

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.