Is the theory of natural numbers and functions $ℕ → ℝ$ decidable under:
- for natural numbers: $\mathrm{succ1}(n) = 2n+1$; $\mathrm{succ2}(n) = 2n+2$; equality
- for functions: pointwise addition and multiplication
- predicate zero: $\mathrm{zero}(f,n)$ iff $f(n) = 0$
(other use of function application $f(n)$ is disallowed)?
More generally, does the decidability hold if in place of $(ℝ,+,⋅,=)$, we used an arbitrary decidable structure $M$ with a distinguished 0 and 1?
S2S (which is equivalent to the above but using functions $ℕ → ℤ_2$) is decidable, and is one of the most expressive decidable theories known. Decidability of $(ℝ,+,⋅,=)$ gives decidability of much of algebra and geometry. Thus, in the quest to find the most expressive decidable theories, it is natural to ask to what extent the two results can be combined. Here is what I have.
If we disallow multiplication, the theory is decidable and is interpretable in S2S. S2S (or just S1S) can interpret $(ℝ,+,<)$ by using binary representation of real numbers, and storing the integer part separately from the fractional part. By using a rearranged binary tree, S2S can interpret a real number on every node, without however the ability to compare arbitrary real numbers stored at different nodes.
If we allow comparison between real numbers stored at different nodes (i.e. test $f(m)=g(n)$ when $m≠n$), the theory is trivially undecidable (even wS1S modified to use function values in an infinite set $X$ with equality can interpret arithmetic), hence the severe limitations above, which can be viewed as using a disjoint copy of real numbers at every node.
An extension is to also allow (pointwise) exponentiation and bounded sine (restriction of $\sin$ to $[-π,π]$). The decidability of this is still open for real numbers, but given a positive answer to the general question, then conditional on decidability, the corresponding extension of S2S is also decidable.
As I reviewed the question, I was able to solve it. I am including it in Q/A format because of its usefulness and also because of the possibility of additional answers, especially if the result is already in the literature, or if given decidability of S2S (as an assumption), there is a generic proof that does not use automata theory.