# Decidability of first-order theory of real closed fields with functions

By a famous theorem of Tarski, the first-order theory of real closed fields is decidable, as it admits quantifier elimination. Can this result be extended so that propositions can be quantified over functions on real numbers? That is, I know that there is a decision procedure for statements like

$$\exists x \in \mathbb{R} ,\forall y \in \mathbb{R}, \exists z \in \mathbb{R}, x +y = zy$$

I'd like to know if there is a decision procedure for statements like

$$\forall f \in \mathbb{R} \to \mathbb{R}, \exists g \in \mathbb{R} \to \mathbb{R}, \forall z \in \mathbb{R}, f(g(z)) = g(f(z)) = z$$

Undecidability results would be just as interesting!

• Can't we define natural numbers? – Kaveh Aug 5 '14 at 16:01
• Let $Ind(f)$ be $$f(0)=1 \land \forall x \ (f(x)=1 \to f(x+1)=1)) \land \forall x \ (f(x)=0 \lor f(x)=1)$$ Then $h=\chi_{\mathbb{N}}$ can be defined by $$Ind(h) \land \forall f \ (Ind(f) \to \forall x \ h(x) \leq f(x))$$ – Kaveh Aug 5 '14 at 16:14
• Right. Second-order logic is (badly) undecidable over any infinite set, one doesn’t even need any a priori structure like a field, as one can quantify it away. – Emil Jeřábek supports Monica Aug 5 '14 at 16:30
• Thanks! Kaveh, if you turn your comment into an answer (and explain that, since you can define $\mathbb{N}$ and its usual operation in this theory, this theory must be undecidable), I will select it as the answer. – jbapple Aug 6 '14 at 0:14

For example, let $Ind(f)$ be the formula: $$f(0)=1 \land \forall x \ \big(f(x)=1 \to f(x+1)=1\big)$$
Now we can define the characteristic function of the set of natural numbers using its universality property as a minimal inductive function: $$Ind(h) \land \forall f \ \big(Ind(f) \to \forall x \ (f(x)=0 \to h(x)=0)\big)$$
(As Emil wrote in his comment we don't even need the language of RCF, we can pick an arbitrary member of the structure as $0$, define a successor function as an injective function whose range lacks our $0$, and then define natural numbers using them. So the undeciability result applies to the second-order language of any infinite structure.)