I want to "translate" an exponent function in predicate logic, but Im having some trouble, because the structure I have is $(\mathbb R, +, \times)$.
And if for example I want to represent $x=5^y$ , I dont have $5$ (which however I managed to get), but how can I represent the multiplication of $5 y$ times? ($y$ can be $0$ or larger)
Thank you.
Kurt Godel showed how you could do this using $\beta$-functions. If you really want to know about this, look for this in the literature, but the rough idea is that for your function $x = 5^y$ we can consider the sequence $5^0,5^1,5^2,...,5^y,...$, and if you have some kind of upper bound to this, i.e. the sequence is $5^0,5^1,5^2,...,5^y,...,5^n$ then it turns out that that finite sequence can be encoded with only two numbers, and the entries of the sequence (i.e. the $5^y$ values that you want) can be recovered using those two numbers and basic addition and multiplication operations (actually, you also do need either a successor function or a constant $1$).
But as Mauro says it is rather complicated, and probably not something you want to use for any kind of practical use. If you want to use exponentiation in practice, I would bite the bullet and just introduce a new symbol for exponentiation ... but at least you can define it recursively in terms of $+$ and $\times$ ... and maybe that's acceptable to you:
$\forall x \: x^0 = 1$ (or $\forall x \: x^0 = s(0)$ if you have $s$ instead of $1$)
$\forall x \forall y \: x^{y+1} = x^y*x$