<p>It's undecidable because we can interpret natural numbers (with addition and multiplication).</p>

<p>For example, let $Ind(f)$ be the formula:
$$f(0)=1 \land \forall x \ \big(f(x)=1 \to f(x+1)=1\big)$$</p>

<p>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)$$</p>

<p>(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.)</p>

CC BY-SA 3.0
2014-08-06T02:14:06.510Z
2014-08-06T02:14:06.510Z
Kaveh
<p><a href="http://gc83.perso.sfr.fr/M2/harrison-real.pdf" rel="nofollow">By a famous theorem of Tarski</a>, <a href="https://en.wikipedia.org/wiki/Real_closed_field#Model_theory:_decidability_and_quantifier_elimination" rel="nofollow">the first-order theory of real closed fields is decidable, as it admits quantifier elimination</a>. 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</p>

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

<p>I'd like to know if there is a decision procedure for statements like</p>

<p>$$\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$$</p>

<p>Undecidability results would be just as interesting!</p>

CC BY-SA 3.0
2014-08-05T16:01:52.977Z
Can't we define natural numbers?
Kaveh
CC BY-SA 3.0
2014-08-05T16:14:08.770Z
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
CC BY-SA 3.0
2014-08-05T16:30:49.353Z
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
CC BY-SA 3.0
2014-08-06T00:14:29.460Z
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
<lo.logic><computability><decidability><model-theory>
Decidability of first-order theory of real closed fields with functions
jbapple
# Decidability of first-order theory of real closed fields with functions

(Asked by: username_0 on 2014-08-05)

[By a famous theorem of Tarski](http://gc83.perso.sfr.fr/M2/harrison-real.pdf), [the first-order theory of real closed fields is decidable, as it admits quantifier elimination](https://en.wikipedia.org/wiki/Real_closed_field#Model_theory:_decidability_and_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!

**Tags:** lo.logic, computability, decidability, model-theory

> **Comments:**
> **username_1**: Can't we define natural numbers?  
> **username_1**: 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))$$  
> **username_2**: 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.  
> **username_0**: Thanks! username_1, 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.  

---

## 1 answers

### Answer by username_1 on 2014-08-06. Score: 5 | Accepted answer

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


---

