Element[Abs[Infinity], Complexes]

returns False, that's right.


Limit[Element[Abs[x], Reals], x -> Infinity]
ForAll[{x}, x == Infinity, Element[Abs[x], Reals]]

returns True,

FullSimplify[expr = Sqrt[1/x^2], Element[x, Reals]]
Exists[{x}, x == 0, Element[%, Reals]] // FullSimplify
Exists[{x}, x == 0, Element[expr, Reals]] // FullSimplify

it seems unreasonable.

  • $\begingroup$ However, Element[Abs[Infinity], Reals] return False. $\endgroup$
    – murray
    Nov 1, 2014 at 21:11
  • $\begingroup$ @murray: Yes, but sometimes Abs[Infinty] with some logical functions will contradiction. $\endgroup$
    – ichaoX
    Nov 2, 2014 at 1:14

1 Answer 1


You are invoking ForAll with vacuous conditions. Compare:

ForAll[{x}, x == x + 1, Element[Abs[x], Reals]]
(* output: True *)

I think that is really all that's going on here. There is no x in the ForAll for which x==Infinity actually returns true, so it spits out true because the "all" in "for all" is the empty set. It's vacuous.

Likewise in the limit, you have a constant sequence True. What is the limit of that? Nobody said the map from set membership to truth values was continuous. Compare:

Limit[x < Infinity, x -> Infinity]
(* output: True *)

I don't see anything fishy going on here, but this is at least somewhat curious a topic. Have I overlooked something, or is it really just business as usual as I seem to say?

  • $\begingroup$ Thank you for your answer. But how to interpret Exists[x,x==0,Element[Abs[1/x],Reals]]//FullSimplify and Exists[x, x == 0, Element[Sqrt[1/x^2], Reals]] // FullSimplify $\endgroup$
    – ichaoX
    Nov 3, 2014 at 11:22
  • $\begingroup$ Abs[1/0] gives you Infinity while Sqrt[1/0] gives ComplexInfinity. The absolute value function returns a real, while square roots of this sort will return complex-valued numbers unless the input is a positive real. (This isn't a Mathematica issue, that's just how square roots work.) $\endgroup$ Nov 3, 2014 at 19:30
  • $\begingroup$ All right. Focus on Exists x==0 return True, it isn't vacuous. $\endgroup$
    – ichaoX
    Nov 4, 2014 at 1:12
  • $\begingroup$ What do you mean "focus on Exists"? I'm not really sure I understand that. The Exists command has three inputs, Exists[x,cond,expr], where cond is a condition on x and expr is the expression you are quantifying. Note that Exists[x,cond,expr] is equivalent to Exists[x,cond&&expr]. When Exists looks at Abs[1/x] it determines that this is real. See also: Reduce[ForAll[x, Element[Abs[1/x], Reals]]] . Because of that, it has reduced x==0&&Element[Abs[1/x],Reals] to x==0&&True, for which x does exist. This simplification will not occur with the Sqrt construction. $\endgroup$ Nov 4, 2014 at 22:20
  • $\begingroup$ I will also point out that using x==0 within an Exists command doesn't make sense. I'm sure you know that, but you can't expect perfect results when threading division by zero and existential quantifiers together. $\endgroup$ Nov 4, 2014 at 22:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.