Can we always know if an algebraic rule over the reals is preserved over the extended reals or not?

Question

Recall a prior posting titled Is there an effective way to generalize this approach of affinely extending the number line?, and especially the accepted answer given to it. So we are working in $\sf ZFC$ with the definitions of operators given in that answer.

The issue I'm asking about here is if we can always figure out when algebra of the presented extended reals departs from alegbra of the reals. There are of course obvious violations, like the real rule "$x + 1 > x$" no longer holds generally over $\hat{\mathbb R}$, but $x +1 \geq x$ does! Another example, $0^0$ seem to confom to $0/0$, i.e. $$0^0 \leadsto k \iff 0/0 \leadsto k$$, also we do have: $\infty^0 \leadsto \infty/\infty; (-\infty)^0 \leadsto -\infty/-\infty$

So, the rule $x^0 \leadsto x/x$, is preserved.

Also $$0^{-\infty}\leadsto 1/0^\infty \leadsto 1/0 \leadsto -\infty, \infty $$

However we don't have: $$ \sqrt[\infty]{0} \leadsto0^{1/\infty} \leadsto 0^0$$, since $\sqrt[\infty]{0} \leadsto r \iff r \in [-1,1]$,

while $0^0 \leadsto r \iff r \in \hat{\mathbb R}$

So here the rule $$k=1/x \implies \sqrt[x]{y} \leadsto y^k$$; no longer applies generally over $\hat{\mathbb R}$.

Given an arithmetical expression $\psi$ that holds over $\mathbb R$, is it always decidable whether this also holds over $\hat{\mathbb R}$?

Answer 1

Of course this depends on the signature (= choice of basic functions) used, but for a wide variety of such the answer will be yes. This is because $(\hat{\mathbb{R}};\overline{\hat{F}})$ is interpretable in $({\mathbb{R}};\overline{{F}})$ for any tuple of functions $\overline{F}$ containing at least $+$ and $\times$ (these let us define ordering). Basically, the definition of $\hat{f}$ I gave in terms of sequences can be reformulated in terms of limit-style language.

The point, then, is that for many choices of $\overline{F}$ the structure $(\mathbb{R};{\overline{F}})$ is decidable and so anything interpretable in it is also decidable. E.g. for $\overline{F}=(+,\times)$ this is due to Tarski.

An interesting near example is $\overline{F}=(+,\times,\mathit{exp})$; the decidability of the resulting structure is an old question of Tarski which is still open. Macintyre and Wilkie showed that it has an affirmative answer assuming Schanuel's conjecture