Translate informal math expressions into predicate logic I'd like to ask for some help with my HW. I have a signature (=, +, *) over $\Bbb{N}_{>0}$
and I need to translate some statements. I've already figured out predicates for "<", "$x$ is prime" and a couple of others, but I've stuck with these two:


*

*"$x$ is $n$th prime number"

*"$x$ is 5 raised to some power"


Main problem in (2) is how to express exponentiation in terms of predicate logic. And as for (1) I have 2 ideas: 1) count prime numbers below $x$ and compare this number to $n$ 2) run predicate recursively on next prime below $x$. But, again, I don't know how to express it properly.
Thank you.
 A: I can help answer the first part of your question. This may not be the most elegant solution, however. We can define a family of predicates $\operatorname{num}_{\leq} (\phi,n)$ for each unary predicate $\phi$ and $n > 0$ true whenever the number of $x$ satisfying $\phi$ is less than or equal to $n$. This is done as follows.
$$\begin{align}
  \operatorname{num}_{\leq} (\phi,1) ~\equiv~ &
    \exists x_1\forall y(\phi(y) \rightarrow y = x_1)\\
  \operatorname{num}_{\leq} (\phi,2) ~\equiv~ &
    \exists x_1 \exists x_2 \forall y (\phi(y) \rightarrow (y = x_1 \vee  y = x_2))\\
  \operatorname{num}_{\leq} (\phi,3) ~\equiv~ &
    \exists x_1\exists x_2\exists x_3 \forall y (\phi(y) \rightarrow (y = x_1 \vee y = x_2 \vee y = x_3)) \\
  \vdots & ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\vdots\\
  \operatorname{num}_{\leq} (\phi,n) ~\equiv~ &
   \exists x_1\ldots\exists x_n\forall y(\phi(y) \rightarrow (y = x_1 \vee \cdots \vee y = x_n))\\
\end{align}$$
Let $\operatorname{prime} x$ be the predicate true if $x$ is prime and false otherwise. For each number $x$, we have the predicate $\phi_x(y) \equiv \operatorname{prime} y \wedge y < x$ true whenever $y$ is prime less than $x$ and false otherwise. If you have abstraction notation available, $\phi_x$ can be written $\lambda y ~ . ~ \operatorname{prime} y \wedge y < x$, which is slightly easier to work with. In either case, the point is that we have a unary predicate. Now we can define the family of predicates $\Phi(x,n)$ true whenever $x$ is the $n$th prime number recursively as follows.
$$\begin{align}
    &\Phi(1,1) \\
    &\Phi(x,n) ~ \equiv ~ \operatorname{prime} x \wedge \operatorname{num}_{\leq}(\phi_x,n-1) \\
  \end{align}$$
For the second problem, recall that $n^m = n \times \cdots \times n$ ($m$ times) whenever $n$ and $m$ are natural numbers. Assuming that you can construct a predicate $\operatorname{exp}(n,m,z)$ true whenever $n^m = z$ and false otherwise, you can test whether a number $z$ is $5$ raised to a power $n$ by testing whether $\operatorname{exp}(5,n,z)$ is true. To this end, it may be useful to recall the recursive definitions of addition, multiplication, and exponentiation, as the predicates in question can be constructed from these.
A: For what I remember this is a not so easy task in order to codify exponetiation and prime sequences one need to use Gödel's $\beta$-function which is a corollary to reminder theorem. 
Hope this helps.
