# Resolve returns False on two contradicting statements

I'm trying to prove an inequality using Mathematica. This is the code leading to the inequality:

T = {{0, pbl*pcharge, 0}, {1, 1 - pbl, psh}, {0, pbl*(1 - pcharge),
1 - psh}};
vecs = Eigenvectors[T];
val = Eigenvalues[T];
pfull = Simplify[(1/(1 + vecs[[1]][[1]] + vecs[[1]][[2]]))];
pbl1 = (1 - phigh)*beta/(lowcons + (1 - pfull - pdead)*M);
psh1 = phigh*(highcons - beta)/(pfull*M);
sols = Simplify[Solve[pbl1 == pbl && psh1 == psh, {pbl, psh}]];
pshex2[highcons_, lowcons_, beta_, phigh_, pcharge_, M_] =
Simplify[sols[[All, 2, 2]]];


However, when I try to use Resolve[] to see if the inequality is true, both the inequality and its negation are resolved as false:

Resolve[ForAll[{highcons, lowcons, beta, phigh, pcharge, M},
highcons > beta > lowcons > 0 && 0 < phigh < 1 && 0 < pcharge < 1 &&
M > 0, D[pshex2[highcons, lowcons, beta, phigh, pcharge, M], M] <=
0], Reals]
Out[1714]= False

Resolve[Exists[{highcons, lowcons, beta, phigh, pcharge, M},
highcons > beta > lowcons > 0 && 0 < phigh < 1 && 0 < pcharge < 1 &&
M > 0, D[pshex2[highcons, lowcons, beta, phigh, pcharge, M], M] >
0], Reals]
Out[1715]= False


Also, FindInstance[] is not able to find an example for the second statement. Is there anything I am doing wrong? I'm very new to Mathematica.

• bugs is a special tag that is supposed to be added only by someone else than the original poster, after verifying the issue. Please do not add this tag to your own posts. – Szabolcs Oct 10 '16 at 8:05
• It does look like a bug to me, please report this to Wolfram Support. – Szabolcs Oct 10 '16 at 9:03
• Sorry! I didn't know that. Sent the issue to Wolfram Tech Support. – Venomouse Oct 10 '16 at 10:37

I found your example a bit hard to follow, so let's write in a form which is more explicit:

expr = First@D[pshex2[highcons, lowcons, beta, phigh, pcharge, M], M];

cond = highcons > beta > lowcons > 0 && 0 < phigh < 1 && 0 < pcharge < 1 && M > 0;


In version 10.0.2 or later (up to 11.0.1):

Resolve[ForAll[Evaluate@Variables[expr], cond, expr <= 0], Reals]
(* False *)

Resolve[Not@ForAll[Evaluate@Variables[expr], cond, expr <= 0], Reals]
(* False *)

Resolve[Exists[Evaluate@Variables[expr], cond, expr > 0], Reals]
(* False *)


ForAll is (surprisingly!) HoldAll so Evaluate was necessary int he first argument.

The second input above is literally the same as the first one except for wrapping the ForAll in Not.

The conditions are clearly fine and there are many combinations of values that satisfy them (FindInstance[cond, Variables[expr]]).

In version 9.0.1:

Resolve[ForAll[Evaluate@Variables[expr], cond, expr <= 0], Reals]
(* True *)

Resolve[Not@ForAll[Evaluate@Variables[expr], cond, expr <= 0], Reals]
(* False *)

Resolve[Exists[Evaluate@Variables[expr], cond, expr > 0], Reals]
(* False *)


It seems clear that there's a bug in v10.0.2 – 11.0.1. Is the result by v9.0.1 correct? That I do not know.

• Thank you for checking this out! Can you please explain why Variables is needed to be used inside Evaluate? – Venomouse Oct 10 '16 at 10:49
• @Venomouse Because ForAll has the HoldAll attribute, which I find quite weird for a symbolic processing function ... I asked about this here, and included examples that show what would happen without Evaluate: community.wolfram.com/groups/-/m/t/937146 – Szabolcs Oct 10 '16 at 10:51

Note that expr is a rational function. If the denominator of expr is zero, then the inequality expr<=0 is neither true nor false -- it is undefined. Hence it is not true that for all values of variables that satisfy cond the inequality expr<=0 is true. If we add the condition Denominator[expr]!=0 then we get the expected result.

Resolve[ForAll[Evaluate@Variables[expr], cond && Denominator[expr]!=0, expr <= 0], Reals]
(* True *)

Resolve[Not@ForAll[Evaluate@Variables[expr], cond && Denominator[expr]!=0, expr <= 0], Reals]
(* False *)