2

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?

Theo Deep
  • 666
  • 4
  • 15

1 Answers1

2

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.

lambda.xy.x
  • 4,918
  • 24
  • 35
  • 1
    'The class of semi-decidable problems is a sub-class of the undecidable problems'. This is the key, thanks a lot. – Theo Deep Nov 24 '21 at 13:21
  • 1
    Sure - I also tried to clear up the NRA question. – lambda.xy.x Nov 24 '21 at 13:27
  • 1
    Thanks a lot! Yes, I also approach the integer problem as if the reals were constrained, so it is more intuitive. Indeed, algebraically closed fields (complex numbers inside) are also decidable, but one cannot use the same approach as from the reals to the integers, because the complexes are not ordered. But if we eliminate inequalities, we could think the same way (reals are complex with more restrictions), am I right? – Theo Deep Nov 24 '21 at 13:34
  • 1
    You can always rewrite the inequality f(x,y,z) < 0 to f(x,y,z) + k = 0 by introducing a new variable k. That approach works both in in integer and real arithmetic. – lambda.xy.x Nov 24 '21 at 13:39
  • And what about complex numbers? `a – Theo Deep Nov 24 '21 at 13:42
  • 1
    I wouldn't say the ordering is a problem - a complex number is just a tuple of two reals and tuples can be ordered lexicographically i.e. ai + b < ci + d iff (a < c) ∨ (a = c ∧ b < d). But reals are uncountable so that brute force enumeration usually doesn't work. I don't know decidability results of the complex number off the top of my head though and would need to look them up. – lambda.xy.x Nov 24 '21 at 13:46
  • 1
    I see.. you ordering gives preference to the real part. What I meant is that I can, in the same way, propose another inequality in which the imaginary part rules. That is way I stated the comparison can be a problem with complex numbers. As for the decidability of complex: 'Alexander Chistov and Dima Grigoriev. Complexity of quantifier elimination in the theory of algebraically closed fields' is a good paper. Thanks for all your responses! – Theo Deep Nov 24 '21 at 14:02
  • 1
    You can also define different orderings on integers.... e.g. x << y iff abs(x) < abs(y) ∨ (abs(x) = abs(y) ∧ x < y) orders by distance from zero first and breaks ties by defining -x << x. I'll have a look at the paper, thanks for the link :) – lambda.xy.x Nov 24 '21 at 16:32
  • 1
    Ah should have looked at both author's names - yeah that's the quantifier elimination paper. – lambda.xy.x Nov 24 '21 at 20:56