# The position of the quantifier

I know this is a logical operation in discrete mathematics.

   Resolve[ForAll[{x, y}, x > y > 0 \[Implies] 1/2^x - 1/2^y < 0]]
(*  No simplification  *)

Resolve[ForAll[{x, y}, x > y > 0] \[Implies] 1/2^x - 1/2^y < 0]
(*  True   *)


What is the difference?

In the second, you are engaging a comparison. See https://reference.wolfram.com/language/tutorial/EnteringFormulas.html

Also you tried other operations

Resolve[ForAll[{x, y}, x > y > 0]! 1/2^x - 1/2^y < 0]
Resolve[ForAll[{x, y}, x > y > 0] \[And] 1/2^x - 1/2^y < 0]
Resolve[ForAll[{x, y}, x > y > 0] \[Or] 1/2^x - 1/2^y < 0]
(*-2^-y+2^-x (\!$$\*SubscriptBox[\(\[ForAll]$$, $${x, y}$$]$$x > y > 0$$\))!<0  *)
(* False    *)
(*   2^-x-2^-y<0   *)


Also compared to

Resolve[ForAll[{x, y}, x > y > 0]! Resolve[1/2^x - 1/2^y < 0]]
Resolve[ForAll[{x, y}, x > y > 0] \[And] Resolve[1/2^x - 1/2^y < 0]]
Resolve[ForAll[{x, y}, x > y > 0] \[Or] Resolve[1/2^x - 1/2^y < 0]]


Resolve[ForAll[{x, y}, x > y > 0]! 1/2^x - 1/2^y < 0]

• Resolve[ForAll[{x, y}, x > y > 0]! 1/2^x - 1/2^y < 0], in this expression, I do not know ! should combine with the former or the latter – tiankonghewo Nov 28 '16 at 3:08