Resolve returns False on two contradicting statements

Question

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]]))];
pdead = Simplify[vecs[[1]][[1]]*pfull];
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.

Answer 1

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.

Answer 2

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