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}}?
{{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