Why does Mathematica claim there is no even prime?

I wonder if this is a bug, or if I'm misunderstanding something:

Exists[n, EvenQ[n] && PrimeQ[n]] // Resolve
(*
==> False
*)


So if I interpret this result correctly, according to Mathematica there does not exist an even prime. However, if given the number directly, it gives the correct result:

EvenQ[2] && PrimeQ[2]
(*
==> True
*)


So did I find a bug in Mathematica (and if so, is it fixed in the latest version)? Or did I misunderstand Resolve?

-

Note: I am not particularly knowledgable in the field of this question, so what I write below may well be wrong.

I don't know whether or not this should be considered a bug, but to my mind this is an instance of a clash of programming and mathematical functionality. To put it differently, predicates (functions ending with Q) seem to be a wrong match for things like FindInstance or Resolve, because of their evaluation semantics. Functions suitable for mathematical transformations tend to return unevaluated when they don't know what to do, which gives the outer functions a chance to further transform them as expressions. OTOH, predicates will always return False immediately when they can not establish the the condition they check is True.

By using Trace[Exists[n,EvenQ[n]&&PrimeQ[n]]//Resolve, TraceInternal->True], one can see that at some point, both EvenQ and PrimeQ evaluate to False, and this is the reason for the result. Moreover, even a simpler request

Exists[n,EvenQ[n]]//Resolve
(*
-->  False
*)


However, this will work:

FindInstance[IntegerPart[n/2]*2==n && n>1 &&n<4 ,n,Integers]

(*
--> {{n->2}}
*)


I wasn't able to make the original request work (I tried using Divisors, but no luck). But my point is that recasting the condition as a set of equations and/or inequalities may increase the chances of success here, because their evaluation semantics is that of the mathematical rather than programming functionality. The borderline seems to be quite blurred, but I think it is there.

-
Note that e.g. FindInstance[EvenQ[n] && n > 10, n, Integers] yields {}. One can carefully say as you did "an instance of a clash of programming and mathematical functionality", but basically that is an incorrect result, so a proper term for this kind of issue is a bug. – Artes Jan 24 '12 at 14:01
Or maybe just that Exists[n, n^2 == 9 && OddQ[n]] // Resolve returns False if we cannot expect for too much from FindInstance – Artes Jan 24 '12 at 14:08
@Artes I disagree. I think this is not an incorrect result, it is an incorrect usage. One should not use predicates for algebraic manipulations and the like. I think I formulated my view on this pretty clearly. I'd agree that the documentation could be more clear about this though. – Leonid Shifrin Jan 24 '12 at 15:26
@Artes I think considering this a bug is similar to considering this Replace[z^4, z^2 -> x] not returning x^2 a bug (although the two situations are not equivalent). The documentation says that EvenQ "gives True if expr is an even integer, and False otherwise." (and this is elaborated in "More information": it must have head Integer and be even). So it's actually doing exactly what it's claimed to do. – acl Jan 24 '12 at 16:57
FindInstance requires a system of equations and inequalites. The only reason it doesn't issue a message with predicates is that they evaluate to False (a valid result from an inequality) before being passed to FindInstance. The documentation clearly states that "expr can contain equations, inequalities, domain specifications and quantifiers, in the same form as in Reduce." – Rojo Jan 24 '12 at 18:02

It has been explained in good detail why your inputs did not work the way you wanted them; however, there is still a way to get what you want:

Resolve[Exists[n, Element[n, Primes] && Mod[n, 2] == 0]]
True

FindInstance[Element[n, Primes] && Mod[n, 2] == 0, n, Integers]
{{n -> 2}}


In general, use Element[n, Primes] whenever you need to make a restriction to prime numbers.

-

Neither Resolve or FindInstance hold their arguments, so they evaluate immediately, and we have:

In[68]:= Exists[n, EvenQ[n] && PrimeQ[n]]

Out[68]= False

In[69]:= EvenQ[n] && PrimeQ[n]

Out[69]= False


So the code isn't really doing what you're expecting it to.

-
Exists does hold its arguments, and is inside Resolve, so I don't buy this (as a direct argument) for Resolve, but agree for FindInstance. If one traces Resolve, as outlined in my answer, one sees that Exists does evaluate the arguments inside it, and that's where it happens. – Leonid Shifrin Jan 24 '12 at 15:29
@LeonidShifrin: I hadn't looked at the attributes on Exists... So then the question is why Exists[n, EvenQ[n] && PrimeQ[n]] evaluates to False instead of returning unevaluated. – Brett Champion Jan 24 '12 at 15:34
Well, if you look at the Trace, you'll see why. But I still blame the use of predicates (in other words, the input code itself). I think they are for programming, because by their nature they will not return unevaluated. At the end, Exists must evaluate its content at some point (at least try)! It does some dummy variables replacement first, but that doesn't help here. – Leonid Shifrin Jan 24 '12 at 15:38
@LeonidShifrin: Ah right. Basically whatever you do to try to symbolically inspect the Q functions will lead to False. – Brett Champion Jan 24 '12 at 15:41
Yes, that's exactly my point! – Leonid Shifrin Jan 24 '12 at 15:44

There are more misleading issues :

FindInstance[EvenQ[n] && PrimeQ[n], n, Integers]
(*
==>  {}
*)


These both results are in v. 7.0.1 as well as in v. 8.0.4

Edit

Even much worse :

FindInstance[OddQ[n] && PrimeQ[n], n, Integers]
(*
==>  {}
*)


In general, Exists and FindInstance work unexpectedly with OddQ, EvenQ, PrimeQ, e.g. :

Exists[n, n^2 == 9 && PrimeQ[n]] // Resolve
(*
==> False
*)

Exists[n, n^2 == 9 && OddQ[n]] // Resolve
(*
==> False
*)

Exists[n, PrimeQ[n] && n < 20] // Resolve
(*
==> False
*)

FindInstance[EvenQ[n] && n > 10, n, Integers]
(*
==>{}
*)


However

FindInstance[n > 10 && n < 20, n, Integers]
(*
==> {{n -> 11}}
*)

Exists[n, n^2 == 9 && n < 0] // Resolve
(*
==> True
*)

Exists[n, 10 < n && n < 20] // Resolve
(*
==> True
*)


Edit 2

Since those issues rather souldn't be called bugs while they still can be misleading, one may blame them on misusing of predicates inside FindInstance and Exists and we could expect more detailed documentation.

-