Take the 2-minute tour ×
Mathematica Stack Exchange is a question and answer site for users of Mathematica. It's 100% free, no registration required.

Consider this example:

FindInstance[Exists[{x, y}, x > 1 && y > 1 && x > Sqrt[x + y]], {x, y}]

which finds values of $x$ and $y$ such that $x>\sqrt{x + y}$. Why does Mathematica output {{x->0, y->0}}? The condition is obviously violated in all three parts: none of $x>1$, $y>1$, or $x>\sqrt{x+y}$ are satisfied by $(0,0)$. What's going on here? Am I misusing FindInstance? Or Exists?

share|improve this question
    
No, it is not a bug, but the documentation is not very clear about this. Please see my answer below –  magma Jan 24 '12 at 16:35
add comment

5 Answers 5

up vote 4 down vote accepted

Resolve[Exists[{x, y}, x > 1 && y > 1 && x > Sqrt[x + y]]] returns True.
This means that the FindInstance does not have to work too hard to find an {x,y} that satisfies the condition.

Note that a less trivial quantifier is something like
q = Exists[x, x > 1 && y > 1 && x > Sqrt[x + y]] and resolving over the reals Resolve[q, Reals] returns y > 1.

So, for the code presented in the question, J.M. is correct and the Exists[] is superfluous.

share|improve this answer
add comment

Your understanding of Exists is wrong. Maybe the best way to explain Exists is by an example:

FindInstance[Exists[y,x==y^2], x, Reals]
(*
--> {{x -> 0}}
*)

This means you seek values of $x$ for which there exists a value for $y$ whose square equals $x$. Obviously $x=0$ is such a value because for $y=0$, we have $x=y^2$. However, $x=-1$ would not be such a value because there's no real number whose square is $-1$. Note especially that in the first argument of Exists, there are variables whose values you don't seek for ($y$ in my example).

To solve your problem, just remove the Exists:

FindInstance[x > 1 && y > 1 && x > Sqrt[x + y], {x, y}]
(*
--> {{x -> 2, y -> 3/2}}
*)
share|improve this answer
    
I agree completely, but it would be nice if Mathematica could give some warning that the input does not make any sense. –  Szabolcs Jan 24 '12 at 11:27
add comment

FindInstance[{x > 1, y > 1, x > Sqrt[x + y]}, {x, y}] works nicely; it looks to me the Exists[] here is superfluous. If you need k instances, use FindInstance[{x > 1, y > 1, x > Sqrt[x + y]}, {x, y}, k].

share|improve this answer
add comment

Another way to see this is to look at:

Reduce[Exists[{x, y}, x > 1 && y > 1 && x > Sqrt[x + y]], {x, y}]

(* ==> True *)

Reduce performs quantifier elimination so you will in general end up with an expression involving only free variables (of course only in those cases for which quantifier elimination can be done, i.e. basically polynomial formulas with real coefficients) When there are no free variables, the expression will be either True or False. Now when you use FindInstance in this case you are in effect asking for an instance of True (in terms of x and y) so any pair of numbers will be an answer. In general,

FindInstance[expr, vars, domain]

is logically equivalent to

FindInstance[Reduce[expr, vars, domain], vars, domain]

although you will not usually get the same answer if you evaluate both (of course this is a very inefficient way to go about finding instances...) Looked at in this way, I think it becomes pretty clear that way that there is no point looking for instances of bound variables since they will be eliminated from the expression before FindInstance starts looking for "instances".

share|improve this answer
add comment

The documentation is not clear about it, but the variables whose instances one is looking for, need to be free variables. This means that they cannot be bound by quantifiers. This makes sense, since bound variables are in essence dummy variables (like those under the integration sign, in calculus) and so it makes no sense to search for them.

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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