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}$?