When I took model theory is an undergraduate, early on we wrestled with trying to state the fundamental theorem of arithmetic in the first order language of arithmetic. The problem was that we needed and unbounded and variable number of quantifiers Depending on each natural numbers factorization in the statement. I.e. For 6 we we need 2 quantifiers but for 110 needs 3. We stopped there because it illuatrated one of the shortcomings of the first order setting. We can quantify over a fixed number of primes and make the statement, but it will be false in general for any fixed prime, obviously.
I was recently refreshing my mind about non-standard models of arithmetic I found out that a form of unique factorization into primes does exist in these setting, but you may have non-standard primes in the factorization. So this means there is some first order sentence capturing the essence of FTA. I want to know what this sentence is. I am certain it will have to use some sort of recursive (=> definable In arithmetic) coding but the details I am unsure of. Can anyone assist me or point me onthe correct direction?
Thank you