The existence of non-effectivizable estimates in the theory of exponential Diophantine equations

The following corrollary of the main theorem of the paper is an example of the estimates mentioned in the title:
There is a particular polynomial $A(a,x_1,\dots,x_{\nu})$ with integer coefficients meeting the following two conditions. Firstly, for every natural value of the parameter $a$ the equation
$$ A(a,x_1,\dots,x_{\nu})=y+4^y $$
has at most one solution in natural $x_1,\dots,x_{\nu},y$. Secondly, for every general recursive (i.e., effectively computable) function $C$ there is a value of the parameter $a$ for which there is a solution $x_1,\dots,x_{\nu},y$ of the above equation such that
$$ \max\{x_1,\dots,x_{\nu},y\}>C(a) $$

The main theorem states that for every recursively enumerable predicate $P(a_1,\dots,a_{\lambda})$ there are expressions $\mathfrak A$ and $\mathfrak L$ built up from natural numbers and variables $a_1,\dots,a_{\lambda}$, $z_1,\dots,z_{\chi}$ by addition, multiplication and exponentation such that
$$ P(a_1,\dots,a_{\lambda})\Leftrightarrow(\exists z_1\dotsb z_{\chi})[\mathfrak A=\mathfrak L_1]\Leftrightarrow(\exists!z_1\dotsb z_{\chi})[\mathfrak A=\mathfrak L_1]. $$
A possibility to obtain similar results for Diophantine equations is discussed.