The language of real closed fields $\mathcal{L}_\text{rcf}$ is a first-order language with operators for $+$, $-$, and $\cdot$, constants for $0$ and $1$, and relations for $<$, $=$ and $>$.

To decide whether such a statement can be classically proven (in, say, ZFC) for the real numbers is easy:

• Use Cylindrical algebraic decomposition (CAD) to compute if it is true or not.
• If yes, then it is classically provable. If not, then it is not classically provable.

But now consider the problem of deciding whether such a statement is provable about the (Dedekind) reals in, say, neutral constructive mathematics. The above algorithm no longer works on the input $\forall x. \forall y. (x = y) \lor \lnot (x = y)$. The algorithm above will state that it is provable since CAD says it is true, but it is in fact not constructively provable since it is the analytic WLPO, which is a constructive taboo. A correct algorithm would declare this statement to be not provable.

So my question is does such an algorithm exist?

I have a feeling though that this should still be computable. Constructive algebra is basically just "fuzzy" classical algebra.

Note though that for first-order arithmetic, the answer is no. A $\Sigma^0_1$ statement is provable iff it is true (whether considering classical or constructive proofs), and deciding this would let you solve the halting problem.

Also note that, constructively, formulas do not in general have a Prenex normal form.