5
$\begingroup$

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

$\endgroup$
  • 5
    $\begingroup$ 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) $\endgroup$ – rm -rf Jul 29 '12 at 17:27
  • 3
    $\begingroup$ @R.M Post that as an answer. There is not going to be a better one. $\endgroup$ – Dr. belisarius Jul 29 '12 at 20:12
1
$\begingroup$

rm-rf answered in comment that

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).

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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