Showing unique prime factorization in first-order logic?

1.8k Views Asked by At

Suppose I have the symbols $\{\neg, \rightarrow, =, <,\cdot, \leftrightarrow,\land, \lor \}$ and functions $Div(x,y)$ ($x$ divides $y$), $Prime(x)$ true if $x$ is a prime, and domain $\mathbb{N}$. How can I construct a formula that expresses the fact that every number greater than 0 has unique prime factorization?

My thought requires the ability to have ellipses, to show for example for a number $k$ it is that $\exists a_1,\ldots,a_k$ such that $a_1^{n_1}\cdots a_{j}^{n_j}= k$ for $j \leq k$. For example, $4 = 2^2$.

Something like this, I don't know.

How can I construct such a formula?