# What domain does Resolve assume by default?

Consider the statement: $\forall x\left(x<7\Rightarrow \exists a\exists b\exists c(a^2+b^2+c^2=x)\right)$

This is true provided the universe of discourse is $\mathbb{N}$

Now I use Resolve as follows to assess the validity of this statement:

Resolve[ForAll[x, Implies[x < 7, Exists[{a, b, c}, a^2 + b^2 + c^2 == x]]]]


and Mathematica returns True. Why? If I did not specify $\mathbb{N}$ as the domain how does Mathematica justify returning True? Is there a way to specify $\mathbb{N}$ as the domain?

The Mathematica documentation makes it clear that the default domain is Complexes. In that domain,

Resolve[ForAll[x, Exists[{a, b, c}, a^2 + b^2 + c^2 == x]]]

True


because, in the complex domain, a^2 + b^2 + c^2 == x is satisfied by

a == Sqrt[x], b == 0, c == 0


To work with Integers, you can write

resolution =
Resolve[Exists[{a, b, c}, a^2 + b^2 + c^2 == x && 0 < x && x < 7], Integers] // Simplify

x == 1 || x == 2 || x == 3 || x == 4 || x == 5 || x == 6


That all the integers x such that 0 < x < 7 are included is easily verified by eye, but to have Mathematica automatically verify it, evaluate

List @@ resolution[[All, 2]] == Range

True