Decidability of S2S with real numbers

Question

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.

Answer 1

Yes, it is decidable, with the following general result for an arbitrary (not necessarily decidable) $M$. Let us interpret an $n$-tuple of $M$-formulas $φ$ with $m$ free variables as a function $φ:M^m→2^n$. A subset of $ℕ×M^k$ is definable from parameters $(A_1,...,A_m)$ iff for a finite set $(φ_1,...,φ_n)$ of $M$-formulas with $k+m$ free variables, the corresponding subset of $ℕ×2^n$ (obtained by applying $φ$) is recognized by a (non-deterministic) tree automaton. Without parameters, these are exactly the tree-regular subsets. Here, the tree is defined using $\mathrm{succ1}$ and $\mathrm{succ2}$. Furthermore, the construction of these formulas is effective (but with an iterated exponential size increase), thus reducing the truth predicate of the theory to that of $M$.

The proof proceeds analogously to the proof of decidability of S2S. However, a reader unfamiliar with that proof might still be able to follow here by reviewing nondeterministic (finite-state) infinite tree automata and relying on their closure under complementation (which is highly nontrivial and also involves exponential size increase). Briefly,
(1) A nondeterministic tree automaton instance splits in two at each branch point of the binary tree (resulting in one instance per branch; the state may depend on the branch chosen), and the automaton accepts iff there is a run (consistent with the state transition table) such that all of the resulting (possibly continuum many) instances accept.
(2) The number of different states is finite, and each state is assigned a priority (an integer). An instance accepts iff the highest priority seen infinitely often is even. (There are also more general acceptance conditions, but this suffices.)

To convert a formula into an automaton, represent it in a prenex form, and then proceed by induction on the number of quantifiers. Numbers (i.e. tree nodes) will be coded by functions (say by being 1 at that number and 0 elsewhere) as the automata cannot receive numbers directly as input.

For a quantifier-free formula $ψ$, $φ$ will consist of the atomic $M$-formulas that are effectively used in $ψ$. Thus, for example given free variables $f,g,h$, if $ψ$ uses $(f+g)(n)=0$ and $(f+g)(m)=0$ and $(f+h)(n)=0$, we can use $φ_1(x,y,z) ⇔ x+y=0$ and $φ_2(x,y,z) ⇔ x+z=0$. To construct the automaton, we can convert $ψ$ to DNF, nondeterministically choose a disjunct at the start, and then verify all of its components in parallel.

Universal quantifiers can be handled through existential quantifiers and closure under complementation.

Just as in S2S, existential number quantifiers can be handled through existential function quantifiers and verification of being a number. For our choice of coding, the latter can be done using a tristate (expect to see the number along the current branch, do not expect to see the number, already saw it) and nondeterministically selecting one path for the number (or we could have included the path in the code), and rejecting if we never see the number along the path, or see a nonzero number elsewhere.

For $∃f \, ψ(f)$, note that the automaton for $ψ(f)$ at node $n$ depends on $f$ only through its current internal state and $φ$. In light of that, set $φ'_i$ to $∃x \, φ(x)=i$. At node $n$, the automaton for $∃f \, ψ(f)$ nondeterministically chooses $i$ such that $φ'_i$ holds and then runs the automaton for $ψ(f)$ until the next node.

Finally, to get decidability assuming decidability of $M$, we plug-in the values of $φ$ and use the decidability of acceptance for nondeterministic tree automata on the zero tree.

Note that each additional quantifier gives an exponential increase in the number of formulas in $φ$ since there are $2^n$ values for an $n$-tuple of statements.