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!
It's undecidable because we can interpret natural numbers (with addition and multiplication).

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.)