Vtyjkyuk

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$