# What is the computational complexity of the first-order theory of real arithmetic?

Tarski proved that the first-order theory of real-closed fields is decidable. Is the exact computational complexity known? The best upper bound I could find is EXPSPACE [1], where it is also conjectured to be EXPSPACE-hard.

Update: The complexity without multiplication, i.e., of FO$$(\mathbb{R},+,<)$$, is complete for the unusual complexity class STA$$(*,2^n,n)$$ [2]. This implies NEXPTIME-hardness.

Here STA$$(s(n),t(n),a(n))$$ is the class of problems solvable by single tape alternating TMs in space $$s(n)$$, time $$t(n)$$, and number of alternations $$a(n)$$, and a $$*$$ means no restriction.

• You could go over all papers citing Ben-Or et al. – Yuval Filmus Feb 1 at 6:33
• This seems a research-level question. – xskxzr Feb 1 at 10:05
• @xskxzr, That sounds plausible. Were you thinking that this should affect how the question is treated? (FYI, research-level questions aren't off-topic here -- I'm probably stating the obvious, though.) – D.W. Feb 1 at 23:45