## Bug in Resolve and Primes?

General discussion about Mathematica features and functionality...
Forum Rules
By using the Wolfram Faculty Program Forum, you agree not to post any abusive, obscene, vulgar, slanderous, hateful, threatening, or sexually oriented material. Wolfram Faculty Program Forum administrators have the right to remove, edit, move or close any topic at any time should we see fit.

Personal Information: Posts in this forum may be viewed by non-members; however, the forum prohibits non-members from viewing your profile. Although your email address is hidden from both non-members and members, your account is initially configured to allow members to contact you via email through the forum. If you wish to hide your profile, or prohibit others from contacting you directly, you may change these settings by updating your profile through the User Control Panel.

Attachments: Attachments are not currently enabled on this forum. To share a file with others on this site, simply upload your file to the online storage service of your choice and include a link to the file within your post. If your school does not offer an online file storage and sharing service, the following sites provide free basic online file storage and sharing: Mozy, FilesAnywhere, Adrive, and KeepandShare.

### Bug in Resolve and Primes?

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?

David_Housman

Posts: 2
Joined: Fri May 13, 2011 7:32 pm
Organization: Goshen College
Department: Mathematics

### Re: Bug in Resolve and Primes?

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:

Let me know if you have any other questions.

-Kathy
Katherine Bautista
Wolfram Research, Inc.
http://www.wolfram.com

Kathy_Bautista

Posts: 182
Joined: Fri Jul 31, 2009 6:24 pm
Location: Mesa, Arizona
Organization: Wolfram Research, Inc.

### Re: Bug in Resolve and Primes?

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?

David_Housman

Posts: 2
Joined: Fri May 13, 2011 7:32 pm
Organization: Goshen College
Department: Mathematics

### Re: Bug in Resolve and Primes?

Hi David,

-Kathy
Katherine Bautista
Wolfram Research, Inc.
http://www.wolfram.com

Kathy_Bautista