# FTA in first order setting

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

-
First-order arithmetic can (in a way I don't know) define exponentiation, which lets then allows (in a way I can explain, if you can't figure it out) uniform coding of tuples, and then also the product of the entries of tuples, which is enough to state FTA. –  Ricky Demer Nov 22 '10 at 17:37

As for proving FTA, it certainly can be done in Peano arithmetic (so FTA holds in all of its models, standard and nonstandard), but also in the much weaker $S^1_2$ if I'm not mistaken. Look up Sam Buss and bounded arithmetic if you're curious about that.