Number theoretical assumptions in metamathematics and axiomatization of PA

Question

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.

Answer 1

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?

In most cases of doing actual metamathematics, the "metatheory" is ordinary informal mathematical reasoning of the kind that was good enough for Euler and Gauss. Naming a particular formal theory as our metatheory is something that happens when we use metamathematical techniques to analyse metamathematics itself. Then, as always, the choice of formal theory depends on which arguments we want to represent in it. It wouldn't be much fun if we decided first to formalize such-and-such metamathematical argument in PA only to discover that PA is not strong enough for that.

(For example, if we want to speak about model theory, decreeing that PA must be the metatheory wouldn't get us very far, because we need some set theory (or something like set theory) to even define what a model is).

To the extent that PA has any particular status here, it is a pragmatic one, which grows out of several facts:

• PA turns out to be strong enough to formalize much of the syntactic reasoning in proof theory.
• On the other hand PA is modest enough that most can readily convince themselves that it must be true about the Platonic integers (to the extent one believes in Platonic integers at all). In contrast, positing that there is a Platonic universe of sets that just happens to satisfy ZFC in particular, is a somewhat wider leap of faith.
• PA is quite simple to describe. There are weaker systems than PA which would also suffice to formalize much syntactic reasoning. But these weaker systems are more complex to define, and they don't even seem to reward us with a system that it is easier to believe in. They generally work by restricting induction to work on formulas of certain shapes; and it is not clear that this makes the resulting system more intuitively tenable.

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.

Well, first because formalizing the meta-level produces results that are interesting in themselves -- e.g. the incompleteness theorems.

Second, and don't discount this: because it's there! Metamathematics is fundamentally an endeavor to build a mathematical model of mathematical reasoning itself -- naturally we'll want to apply that goal to the example of mathematical reasoning that would be closely on our mind while doing so, namely metamathematics itself.