Showing unique prime factorization in first-order logic? 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?
 A: The challenge here is that there is no a priori bound on the number of factors. So, to express the fundamental theorem of arithmetic in a first-order theory such as Peano arithmetic, you first need to show that the theory is able to express the idea of quantifying over finite sequences. The machinery to do this is well understood; one commonly used method is the $\beta$ function introduced by Kurt Gödel.
The general idea is that the final sentence will say "for every $n > 1$ there is a finite sequence $\sigma$ such that (1) each number appearing in $\sigma$ is prime, and (2) $n$ is the product of the numbers appearing in $\sigma$."
A: Let us first define $\text{Prime}(n)$ to be an expression that is true iff $n$ is prime:
$$ \text{Prime}(n) \stackrel{\text{def}}{⟺} ∀x∀y\Big[ (x×y=n) ⟶ (1<n<x+y) \Big] $$
This works because the only pair factors of $n$ who's sum is greater than $n$ is $1$ and $n$ itself.
Now let us define $d$ divides $n$ ($d|n$):
$$ d|n \stackrel{\text{def}}{⟺} ∃x \big[d×x=n\big]$$
Now note that a number is either $0$, $1$, prime, or a composite number (divisible by a prime):
$$ ∀x\Big[(x<0)∨\text{Prime}(x) ∨ ∃y∃z\big[(y×z=x)∧\text{Prime}(y)\big]\Big] $$
So now we know that every composite number $x$ has a prime factor $y$ and another factor $z$. If $z$ in a prime number, $x$ is the product of 2 prime numbers.
Sorry, I'm not entirely sure where to go from here, but I thought I'd post this anyway in case it's any use to you. Maybe I'll come back and edit it later.
