# Incompleteness of FindInstance

I've been playing around with Resolve and FindInstance. I know that Resolve should always be decidable when the domain is Reals by Tarski's theorem, but I don't know about FindInstance. I tried using FindInstance to find a lower bound on the absolute value of a real number, but it didn't succeed.

(* First-order logic characterization of absolute value. a = |x|. *)
MyAbs[x_, a_] := (x > 0 \[Implies] a == x) ∧ (x <= 0 \[Implies] a == -x)

(* Returns True, so yes there is a lower bound. *)
Resolve[Exists[l, ForAll[{x, a}, (MyAbs[x, a]) \[Implies] a >= l]], Reals]

(* Returns True, so yes 0 is a lower bound. *)
Resolve[ForAll[{x, a}, (MyAbs[x, a]) \[Implies] a >= 0], Reals]

(* Returns {}, so Mathematica can't find a specific lower bound. *)
FindInstance[ForAll[{x, a}, (MyAbs[x, a]) \[Implies] a >= l], {l}, Reals]

(* Using the standard Abs also returns {} *)
FindInstance[ForAll[x, Abs[x] >= l], {l}, Reals]


Why is FindInstance not returning {{l -> 0}}?

-
It does return {{l -> 0}} for me. I think this is due to a version difference. Mine is 8.0.4. There have been several such errors and differences between 8.0.0 and 8.0.4 (way too many for a minor revision) –  rm -rf Jul 29 '12 at 17:27
Thanks, this was the problem. –  jnhnum1 Jul 29 '12 at 18:17
@R.M Post that as an answer. There is not going to be a better one. –  belisarius Jul 29 '12 at 20:12

It does return {{l -> 0}} for me. I think this is due to a version difference. Mine is 8.0.4. There have been several such errors and differences between 8.0.0 and 8.0.4 (way too many for a minor revision).