Bug in Resolve and Primes?

[David_Housman]

I would have expected that the following two commands would return True and False, respectively. Instead, they are left in an unevaluated form.

Code: Select all

Resolve[ForAll[x, Implies[x == 2, Element[x, Integers]]]]
Resolve[ForAll[x, Implies[x == 2/3, Element[x, Integers]]]]

Mathematica should be able to handle the above commands because it can handle the logically equivalent forms below that make use of FindInstance.

Code: Select all

FindInstance[! Implies[x == 2, Element[x, Integers]], {x}] == {}
FindInstance[! Implies[x == 2/3, Element[x, Integers]], {x}] == {}

Is there a bug with Resolve or is there something I do not understand?

Worse, the following two commands return False and True, respectively, although they should both return True:

Code: Select all

Resolve[ForAll[{a, b}, Element[a, Primes] && Element[b, Primes], Implies[a^2 == b^2, a == b]]]
FindInstance[Element[a, Primes] && Element[b, Primes] && ! Implies[a^2 == b^2, a == b], {a, b}] == {}

Perhaps there is a problem with Primes or my understanding of Primes?

[Kathy_Bautista]

Hello David,

I spoke to one of our Technical Support engineers, who mentioned that Resolve only attempts to remove the quantifier from the statement and simplify the statement. This is however a very good suggestion on how we can improve this functionality for a future version of Mathematica and he has forwarded this suggestion directly to the developers.

He also responded with the following...

"The customer may also be interested to know that FindInstance and Resolve work in very different ways. The internals are complicated, but the fundamental algorithm underlying each is incredibly different and what each does is a very different thing. Therefore the abilities of one of them does not really imply what the abilities of the other function should be in any way."

Here are the links to the documentation pages on both of these functions:

• Resolve
• FindInstance

Let me know if you have any other questions.

-Kathy

[David_Housman]

Thank you for your response. Although I had read the documentation before, I decided to read it again.

Since every integer is a rational and since Mathematica documentation states, "Resolve[expr] can in principles (sic) always eliminate quantifiers for any Boolean expression expr," the following command should output True. Instead it returns the unevaluated expression.

Code: Select all

Resolve[ForAll[x, Implies[Element[x, Integers], Element[x, Rationals]]]]

Since Mathematica documentation states, "ForAll[x,cond,expr] is equivalent to ForAll[x,Implies[cond,expr]]," the following command should be equivalent to the proceeding command. Instead it returns True.

Code: Select all

Resolve[ForAll[x, Element[x, Integers], Element[x, Rationals]]]

The following command also outputs True.

Code: Select all

Resolve[ForAll[x, Implies[Element[x, Integers], Element[x, Rationals]]], Integers]

Based on this, it appears that the first command is unable to resolve the Boolean expression over the complexes, and so the second command is recognizing by the condition that the resolution should be over the integers.

While I would be amazed if the Mathematica function Resolve could "always eliminate quantifiers for any Boolean expression" as stated in the documentation, it is unsettling to find that it does not eliminate such an easy quantifier as in the first command. Or am I missing something in my logic?

The reason I find the above unsettling is because I planned to introduce Mathematica to my Discrete Mathematics students as a great way of computing mathematically defined concepts. Specifically, I had planned to define the following function, based on the first command above, for determining whether a set X is a subset of a set Y.

Code: Select all

Subset[X_, Y_] := Resolve[ForAll[x, Implies[Element[x, X], Element[x, Y]]]]

The corresponding mathematical definition comes directly from the text we are using. Unfortunately, as shown earlier, this function will not always return a Boolean value. I will instead provide a definition based on the second command, but that will not be as direct as the one based on the first command.

What is more unsettling is that the following command (as noted in my original post) returns False. This is WRONG!

Code: Select all

Resolve[ForAll[{a, b}, Element[a, Primes] && Element[b, Primes], Implies[a^2 == b^2, a == b]]]

How can I trust Mathematica on more complicated calculations when it gets a simple one wrong?

[Kathy_Bautista]

Hi David,

I just sent you an email about this issue.

-Kathy