Let f(x)= 2^([log₂x]2)           (1) for x>0, and f(0)=0. Here [log₂x]=i ⇔ 2ⁱ≤ x<2ⁱ⁺¹. If 2ⁱ≤ x<2ⁱ⁺¹ then f(x)=2⁽ⁱ²⁾. This f is not interpretable in <N, <, +, 2^x> because the first-order theory of <N, <, +, 2^x, f> is undecidable.

The same quantifier elimination holds for f(x)= 2^P([log₂x])           (2) where P(x)=d_nxⁿ+d_n-1x^n-1 +…+d₁x+d₀,
d₀,d₁,…,d_n are integer numbers, n>1, and d_n>0.

The same quantifier elimination also holds for f(x)= m^g([log_mx])           (3) where m is a natural number, m>1, g is a unary function from natural numbers into natural numbers, g is periodical by module m for any positive natural m, and g(n+1)−g(n)>n.

Previous page
Next page