This question has probably come up many times before so I will make sure to be explicit as possible for the things I am confused about and I hope that you can help me!
The main problem for me is the justification of number-theoretical results in proofs in metatheory.
I am reading Kleene's "Introduction to Metamathematics". At one point he starts to introduce primitive recursive functions to prove one lemma for Godel's theorem. There, he says that we can use prime factorization theorem that says that every natural number has unique prime factorization. This is to be used in a lemma for a metamathematical proof about formal theory. What it seems to be is that we are taking some results from number theory which we want to formalize to prove statements in metatheory. Now, as far as I understand, formalization is used to ensure that proofs are purely syntactical and there is no intuition necessary to prove one or the other thing. On the other hand, proofs in metatheory are not really proofs but just intuitive presentations of some certain arguments that we assume to be true intuitively. This seems to contradict the fact that we use number-theoretical results in metatheory.
Question 1: I have read that metatheory cannot be built on "nothing" and I agree with that - we must be able to know how to write strings of symbols, "add" them, distinguish them and so forth. I have seen answers to some questions that have the point of view that metamathematics satisfies some axiomatic system (intuitive axiomatic system) such as Peano Arithmetics. Is it true that most "logicians" assume that metatheory satisfies Peano axioms? If that is the case, is there some transition or intuitive argument for why string operations should satisfy PA?
Question 2: I suppose that many people will answer that we assume PA for metatheory in order to prove results like Godel's theorem. But then I am confused about why do we even want to axiomatize number theory? If I understand correctly then axiomatization was created in order to make explicit all of the assumptions about theories that describe non-intuitive concepts, like theory of sets, theory of category of categories. Then the proofs should be independent of intuition and be only purely syntactically done. On the other hand, metatheory is something very intuitive and should be supported by most mathematicians. If we already use PA in metatheory and, therefore, say that it is intuitively clear, what is the point of formalizing it? I am willing to accept that we take PA intuitive and valid for metatheory and then formalize set theory and things like that which have non-intuitive meanings like non-countable, non-measurable sets etc. But I cannot seem to find reasons why would we want to formalize PA in the first place.
I hope I made my questions sufficiently explicit, but please let me know if I should elaborate on the questions more. I would appreciate any suggestions or comments.