Reference textbook for Godel's incompleteness theorems proved in PRA or PA metatheory

Question

I think one of my recent misunderstandings and confusions is about how can metatheory be PRA or PA if those are "formal theories". This confusion arose when I started reading Godel's theorem which used prime number decomposition theorem. So, I think maybe if I read how Godel's incompleteness theorem is proved rigorously when metatheory is PRA or PA then I will understand what it means.

I would be happy if you could recommend some reference texts which treat Godel's incompleteness theorems with as many details as possible about what is metatheory, what do we assume in metatheory, how do we rigorously prove things in metatheory and what it means for metatheory be PRA or PA.

Answer 1

I suspect you might be approaching this the wrong way.

The first thing to do is to get your head fully around a standard textbook proof of Gödel's theorem for PA -- you have many good ones to choose from! Find a textbook that suits (old-school Mendelson, friendlier Epstein/Carnielli, Boolos/Burgess/Jeffrey, Leary/Kristiansen, mine: details of these books in §4.2 of the Study Guide https://www.logicmatters.net/resources/pdfs/TeachYourselfLogic2017.pdf)

These textbook proofs of course proceed in everyday informal mathematics. Having got your head round one of them, stand back from that proof and ask yourself: what resources does it bring to the party? And you'll see that the answer is "not a lot", a bit of theory of syntax, a bit of theory of primitive recursive functions, and that's about it.

Of course, "you'll see" is a bit arm-waving. So you need to think twice and carefully check through. And yes. After checking carefully, you'll see that the needed resources are indeed weak.

Now, if you are VERY pernickety, or very skeptical, or just like a challenge, you can confirm that the needed resources really are weak by formalising the argument in a weak theory (PRA is enough). It's good to know that it can done (but did anyone really doubt that it could be done?). But that will just confirm what you should already have seen from carefully following through the informal textbook proof. It will not give you any additional understanding of Gödel's theorem itself (not the sort of additional insight that comes from thinking e.g. about different proof strategies) or any additional understanding of its philosophical/foundations-of-maths significance.