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!

  • $\begingroup$ Can't we define natural numbers? $\endgroup$
    – Kaveh
    Aug 5 '14 at 16:01
  • 1
    $\begingroup$ 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))$$ $\endgroup$
    – Kaveh
    Aug 5 '14 at 16:14
  • 1
    $\begingroup$ 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. $\endgroup$ Aug 5 '14 at 16:30
  • $\begingroup$ 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. $\endgroup$
    – jbapple
    Aug 6 '14 at 0:14

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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.