9
$\begingroup$

It's well known that sentences about the real closed field can be decided by algorithm and the complexity of this is about $d^{2^{O(n)}}$ where $d$ is the product of the degrees of polynomials in the sentence. See here

Now adding an operation such as the $\sin$ function to the field structure leads to the ability to define natural numbers (and so now its undecidable).

Other operations such as adding an $\exp$ appear to be open problems (we can't prove if it is decidable or not, let alone having an algorithm which provably runs in finite time).

So I was curious, do we know ANY other relations which can be added to the underlying structure such that we still end up with a decidable theory AND we are able to prove new sentences which were not expressible before.

I would expect it should be possible to construct an ordinal-indexed hierarchy of such decidable theories, each of whose runtime for deciding expressions is naturally related to the ordinal it is indexed by and whose limit approaches the theory of the natural numbers.

But that is just wishful thinking for now ^

I guess I'm just curious if anyone knows how to make a "bigger" theory than the real closed field which is still decidable.

Improve this question
$\endgroup$
2
  • 2
    $\begingroup$ I think this is a good question, but I'm a bit confused by the phrasing: "AND we are able to prove new sentences which were not expressible before" seems a trivial condition. You're talking about theories of the form $Th(\mathbb{R};+,\times, [thing])$ for some new relation/function $[thing]$, right? In that case, you'll trivially be able to prove lots of newly-expressible things in this theory, since any theory of such a form is complete. $\endgroup$
    – Noah Schweber
    Commented Jan 10, 2023 at 18:48
  • $\begingroup$ Well “thing” also has a semantic meaning so we might invent some new sentence but actually that sentence is equivalent to something in the original real closed field. Ex: if “thing” was a new relation that was identical to the $<$ relation. But that case is obvious “thing” could seem like it’s new but really it’s not. I might even say we know “thing” is different BECAUSE the higher runtime of decidability tells us so. $\endgroup$
    – Sidharth Ghoshal
    Commented Jan 10, 2023 at 19:05

2 Answers 2

Reset to default
12
$\begingroup$

Thanks to a 1958 paper by Abraham Robinson (whose impetus was a question of Alfred Tarski), an example of such a theory that properly extends RCF is the theory of the structure $(\mathbb{R},~+,~\cdot,~A)$, where $A$ is the collection of algebraic real numbers.

More generally, Robinson's proof shows that the theory of structures of the form $(\mathbb{R},~+,~\cdot,~F)$ is decidable for any real closed subfield $F$ of the field or reals.

A free copy of Robinson's paper can be found here.

Improve this answer
$\endgroup$
3
  • $\begingroup$ The paper appeared in 1959. Fund. Math. 47 (1959), 179–204. $\endgroup$
    – Philip Ehrlich
    Commented Jan 10, 2023 at 23:28
  • 3
    $\begingroup$ Can it be iterated - that is, if $A_1\subseteq ... \subseteq A_n$ are real closed subfields of $\mathbb{R}$, is $(\mathbb{R};+,\cdot, A_1,...,A_n)$ decidable? $\endgroup$
    – Noah Schweber
    Commented Jan 10, 2023 at 23:45
  • $\begingroup$ @NoahSchweber Unfortunately I do not know the proof of Robinson's theorem well enough to answer your question, perhaps this should be a new question. $\endgroup$
    – Ali Enayat
    Commented Jan 11, 2023 at 8:57
8
$\begingroup$

You can add a predicate for the integer powers of two and retain decidability. There was a previous question about that theory, and my comment there links to an algorithm for quantified elimination in that language.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .