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?