# Is the First-Order Theory Over Reals with Uninterpreted Functions Decidable?

While I understand that the first-order theory of real-closed fields $$(\langle \mathbb{R}, +, \cdot, < \rangle)$$ is decidable via Tarski's theorem and quantifier elimination, I'm curious about the impact of adding uninterpreted functions.

I also know that by Nelson and Oppen, the quantifier-free fragment of the union of decidable theories is decidable. However, I am unsure if quantifier elimination is possible when the function's input is quantified.

Specifically, does the first-order theory over the reals extended with uninterpreted functions remain decidable?

### Example:

To illustrate, consider the following statements involving uninterpreted functions $$\alpha$$ and $$\beta$$:

$$\forall (t \in \mathbb{R}) \left( \alpha(t) = 1.0 \Rightarrow \exists (t_1 \in \mathbb{R}) \left( t_1 > t \land t_1 < (t + 10.0) \land \beta(t_1) = 2.0 \right) \right)$$

Would such statements be within a decidable theory when $$\alpha$$ and $$\beta$$ are uninterpreted functions?

I appreciate any insights or references to relevant literature on this topic!

• Exactly what is an uninterpreted function? Commented Jul 18 at 10:52
• @Lucenaposition: "uninterpreted function symbol" is standard terminology for a function symbol that doesn't appear in any axioms (so that it's interpretation is unconstrained by the theory). Commented Jul 18 at 20:55
• @RobArthan Interesting - I've never heard this terminology. Do you have a reference? Commented Jul 18 at 23:03
• @AlexKruckman: just google it. I get this result: en.wikipedia.org/wiki/Uninterpreted_function Commented Jul 19 at 21:20

Letting $$\alpha$$ be a "fresh" function symbol, consider the sentence $$\theta$$ which says that $$\alpha^{-1}(0)$$ defines an integer part of the universe; that is, $$\alpha^{-1}(0)$$ is a discrete ordered ring and each $$x$$ is within $$1$$ (or even $$1\over 2$$) of some element of $$\alpha^{-1}(0)$$. Basically, $$\theta$$ "carves out" a part of the universe which looks like the integers. The theory of discrete ordered rings is known to be incomplete, essentially for the same reason as Robinson arithmetic (although we have to be careful since we don't have induction); in particular, letting $$T$$ be the theory in your post, we get that the set of $$T$$-theorems of the form $$\theta\rightarrow\sigma$$ for some $$\sigma$$ is not computable and so $$T$$ is not decidable.