Determinism versus nondeterminism with arithmetic tests and computation

Abstract

For each natural number d we consider a finite structure M d whose universe is the set of all 0,1-sequence of length n=2 d, each representing a natural number in the set [0,1,...,2 n-1] in binary form. The operations included in the structure are the four constants 0,1,2 n - 1,n, multiplication and addition modulo 2 n, the unary function min[2 x, 2 n-1], the binary functions ⌊x/y⌋ (with ⌊x/0⌋ =0), max(x,y), min(x,y), and the boolean vector operations ∧, ∨, ¬ defined on 0,1 sequences of length n by performing the operations on all components simultaneously. These are essentially the arithmetic operations that can be performed on a RAM, with wordlength n, by a single instruction. We show that there exists a term (that is, an algebraic expression) F(x,y) built up from the mentioned operations, with the only free variables x,y, such that for all terms G(y), which is also built up from the mentioned operations, the following holds. For infinitely many positive integers d, there exists an a ε M d such that the following two statements are not equivalent: (i) m d |= ∃x, F(x,a), (ii) M d |= G(a)=0. In other words, the question whether an existential statement, depending on the parameter a ε M d is true or not, cannot be decided by evaluating an algebraic expression at a. Another way of formulating the theorem, in a slightly stronger form, is, that over the structures M d, quantifier elimination is not possible in the following sense. Let M be a first-order language with equality, containing function symbols for all of the mentioned arithmetic operations. Then there exists an existential first-order formula φ(y) of M, containing a single existential quantifier and the only free variable y, such that for each propositional formula P(y) of M, we have that for infinitely many positive integers d, φ(y) and P(y) are not equivalent on M d, that is, M d |= ¬∀y,φ(y) ↔ P(y). We also show that the theorem, in both forms, remains true if the binary operation min {x y, 2 n-1} is added to the structure M d. A general theorem is proved as well, which describes sufficient conditions for a set of operations on a sequence of structures k d, d=1,2,... which guarantees that the analogues of the mentioned theorems holds for the structures k d too. © 2012 ACM.