In Z3 (Python), I solved the following:
y1,y2,x = Ints('y1 y2 x')
univ = ForAll([x], (y1<y2+x*x))
phi = Exists([y1,y2], univ)
solve(phi)
Note that the encoding does not make sense, just playing.
The point is that the result totally blew my mind, since it returned a result! This was surprising since I have been studying first order theories and, as far as I knew, LIA is decidable, whereas NIA was not (the same happens with rationals). The result was [], by the way: i.e. valid.
So I searched about this problem in this side and found (How does Z3 handle non-linear integer arithmetic?), where it is Leonardo de Moura himself who responds the following: if a formula has a solution, we can always find it by brute force. That is, we keep enumerating all possible assignments, and testing whether they satisfy the formula or not. This is not that different from trying to solve the Halting problem by just running the program and checking whether it terminates after a given number of steps.
Okay, so I understand NIA is semi-decidable. Is it right? However...
In (https://hal.archives-ouvertes.fr/hal-00924646/document) the following is stated: Gödel showed that (NIA) is an undecidable problem.
Also, in (Quantifier Elimination - More questions), the same is stated: NIA does not admit quantifier elimination. Moreover, the decision problem for NIA is undecidable.
Then, is NIA undecidable or semi-decidable? Obviously, I see there can be some solutions. So does Gödel mean undecidable in the sense that is not decidable (but saying nothing about semi-decidability)?
Are there fully undecidable LIA fragments? For instance, in NRA, in (Z3 support for nonlinear arithmetic) it is stated that only Nonlinear polynomials are decidable (for Z3).
Can anyone provide some clarification?
The class of semi-decidable problems is a sub-class of the undecidable problems.
Since we are looking for integer solutions, there is an easy way of enumerating the solutions parametric to some natural number n: first consider all values of variables such that the sum of their absolute values is 0, then 1, etc. and check if the equation holds. This strategy covers all possible values such that eventually the algorithm will return a solution if it exists or keep on enumerating indefinitely. This is the definition of a semi-decidable algorithm so if we have an undecidability result it is semi-decidable at worst.
The actual undecidability proof for NIA is Matyasevich's Theorem - an answer to one of Hilbert's famous questions.
Decidability of a class means that every instance is decidable. Since LIA is decidable there is no undecidable counter-example.
By the way: real closed fields are a decidable theory (the proof works by replacing quantified variables by values - this is an example of quantifier elimination) which means NRA is also decidable. This was a bit counter-intuitive for me since integer artihmetic felt more simple. Nowadays I think of it as the reals having more possible solutions where the additional constraint that the solution is an integer is the hard part.