I am reading Kleene's "Introduction to Metamathematics" and in chapter 45 he mentions that "a given positive integer can be factored into a product of prime factors which is unique to within the order of the factors."
I am okay with assuming that in metatheory we can use natural numbers (which could be just |, ||, |||, ||||, ...) and I am okay with assuming that in metatheory we can use primitive recursive functions because for each choice of natural numbers as input for these functions I am certain that I am able to compute the value of a function in finite amount of steps.
Question 1: How can one prove/argue that fundamental theorem of arithmetic holds in a metatheory where primitive recursive functions are allowed?
I know that multiplication is primitive recursive and that it is possible to construct function $Pr(a)$ which outputs $0$ when $a$ is a prime number and $1$ when it is not a prime number, this function is also primitive recursive.
I assume that it means that multiplication of $Pr(i)$ finite amount of times (where $i$ can change) is also primitive recursive function. But what should I do next?
I think the first step would be proving that the order of multiplication doesn't matter for the output result. How can I show that? Do I just take some natural numbers and two different primitive recursive functions $(a \cdot b) \cdot c$ and $a \cdot (b \cdot c)$ and show they are equal? Why does such "proof" works? Because primitive recursive functions can always be calculated in finite steps and thus one can always check that it is indeed true?
Then, I guess I would have to translate the standard informal proof of existence and uniqueness. I am not sure how to do that.
I would appreciate all kinds of comments, suggestions and references to this topic.
Remark: Probably many of you will think that this kind of question is "overthinking" the basic principles, because we have to assume something, for example, that natural numbers work. But isn't the fact that we formalize theories is exactly against the attitude of appealing to intuition? Then, I think the only intuition would be in metatheory in a form that "intuitively I believe that primitive recursive functions can be evaluated in finite steps and thus checked". But I do not think that the fundamental theorem of arithmetic is intuitive or should be considered intuitive, even though it probably was in the time of Gauss (or is to many of us nowadays). Ideally, I would like the proof of it to be with as less intuition as possible. My reason for such question is that I want to understand Godel's incompleteness proofs which are metatheoretical proofs (as far as I understand them).