The [Tarski–Seidenberg theorem](https://en.wikipedia.org/wiki/Tarski%E2%80%93Seidenberg_theorem) asserts that the projection of a semialgebraic set is also a semialgebraic set. My question is whether this is provable in constructive mathematics.

First, let me formalize what this means constructively. Let $\phi(x_1,\dots,x_n,c_1,\dots,c_m)$ be a quantifier-free formula in the language with $+$, $\cdot$, and $<$. Then $$\{(x_1,\dots,x_n) \in \mathbb R^n : \phi(x_1,\dots,x_n,c_1,\dots,c_m)\}$$ is a semialgebraic set for any $c_1,\dots,c_m \in \mathbb R$ ($c_1,\dots,c_m$ are called *parameters* or *constants*). This is the same as the usual definitions when using classical mathematics.

For any set $S \subseteq R_{n+1}$, its projection is $$\{(x_1,\dots,x_n) \in \mathbb R^n : \exists x_{n+1} \in \mathbb R. (x_1,\dots,x_n,x_{n+1}) \in S \}$$

The Tarski–Seidenberg theorem states that if S is semialgebraic, its projection is semialgebraic.

We might also consider if S's co-projection $\{(x_1,\dots,x_n) \in \mathbb R^n : \forall x_{n+1} \in \mathbb R. (x_1,\dots,x_n,x_{n+1}) \in S \}$ is semialgebraic. Classically the Tarski–Seidenberg theorem implies this too, but constructively the analogous statement talking about co-projections is different. I'll call this the "co-Tarski–Seidenberg theorem" and am interested in its constructive provability as well.

If they are not constructively provable, I am also curious of how strong they are. For example, does the Tarski–Seidenberg theorem or the co-Tarski–Seidenberg theorem imply the [fundamental theorem of algebra](https://ncatlab.org/nlab/show/fundamental+theorem+of+algebra#in_constructive_mathematics).

---

Classically we can prove that the semialgebraic sets on $\mathbb R^n$ form a [Boolean algebra](https://en.wikipedia.org/wiki/Boolean_algebra_%28structure%29), but constructively we can only show that they form a [Heyting algebra](https://en.wikipedia.org/wiki/Heyting_algebra?wprov=sfla1).

If we restrict our attention to the algebraic real numbers, I'm pretty sure the Tarski–Seidenberg theorem is constructive since working with the algebraic numbers isn't much different constructively (in particular, they have decidable equality). In fact, I think we can represent Tarski–Seidenberg theorem over the algebraic numbers as a $\Pi^0_2$ statement that can thus be made constructive using the [Friedman translation](https://en.wikipedia.org/wiki/Friedman_translation).

However, working with $\mathbb R$ there are significant differences that probably break the original proof. For example the sets $\{x \in \mathbb R: \lnot (x = 0)\}$ and $\{x \in \mathbb R : (x > 0) \lor (x < 0)\}$ are semialgebraic sets that are obviously equal classically but can't be proven equal constructively (but could be proven equal if we replace $\mathbb R$ with the algebraic numbers).

(Also see *https://mathoverflow.net/questions/468849/is-it-decidable-whether-a-statement-about-reals-in-the-language-of-ordered-ring* for a closely related question.)