Using Simplify on a consistent system returns False

Question

Bug introduced in 8.0 and fixed in 10.3.

---

It's late, but am I missing something here? Why should two independent equations, which together are consistent, Simplify to False?

ClearAll[x, y];
Simplify[y == 0 && x^2 == -1]
(*
  False
*)

Mathematica thinks they're consistent:

Solve[y == 0 && x^2 == -1]
(*  {{x -> -I, y -> 0}, {x -> I, y -> 0}}  *)

Individually, each does not simplify to False:

Simplify[y == 0]
Simplify[x^2 == -1]
(*
  y == 0
  x^2 == -1
*)

Such behavior turns up with other equations as well, but the more complicated they are, the less likely it seems that the conjunction will simplify to False. So far I can only get it to happen when at least one of the equations has complex roots.

It seems so basic, I felt like I was missing something. As I write this question, I'm feeling more and more it's a bug. Any ideas what is going on?

V10.1, Mac OSX 10.10.3

---

Confirmed by WRI (CASE:3370522).

Answer 1

Just to summarize my understanding: First of all, the documentation states that Simplify assumes that variables are real when they occur algebraically in inequalities. Clearly, there are no inequalities in the logical expression y == 0 && x^2 == -1, and therefore x and y should be assumed to be general complex numbers. If they were real, then the simplification to False would be justified, because -1 has no real square roots.

When an expression can evaluate to True or False for different generic values of the variables, consistent with the assumptions, Simplify should leave it unevaluated. This is the case here if x and y are complex.

It therefore appears that the presence of And in the expression erroneously triggers the assumption of reality. The same happens when Or is present, as seen here:

Simplify[y == 0 || x^2 == -1]

(* ==> y == 0 *)

This simplification is only correct if one assumes x to be real so that the second clause is False. To see this, look at the result of Refine instead:

Refine[y == 0 || x^2 == -1, x ∈ Reals]

(* ==> y == 0 *)

The documentation states that Refine is one of the transformations called by Simplify. But without the assumption above, we get the correct result

Refine[y == 0 || x^2 == -1]

(* ==> y == 0 || x^2 == -1 *)

This means that before calling Refine, there is some processing inside Simplify that amounts to adding the assumption x ∈ Reals.

Whatever this additional processing is, it was absent in version 5.2 and is present in versions 8 and above. This fact leads me to conclude that it's a bug.

Also: the bug can't be removed by explicitly stating the assumption of complex variables:

Simplify[y == 0 || x^2 == -1, x ∈ Complexes]

(* ==> y == 0 *)