I’ve read quite a few pop math books over the years with descriptions of the incompleteness theorem and I think I understand most of the broad details, but some still elude me. Specifically, these three below. I’m using Peano Arithmetic like most popularizations do.
As I understand it, the incompleteness theorem works in part because one can interpret the sentences of PA as talking about (or modeling) natural numbers (which I will call model A) and that is obviously the intended interpretation. However, as Gödel famously demonstrated, PA can also be interpreted as proving truths about strings of PA, which I will call the meta-model M.
Finally as I understand it, the completeness of First Order Logic means that any sentence which is true in every model is provable. So in other words, every model of the axioms need to agree on the truth value of the provable sentences. However, they do not have to agree on the unprovable sentences because those unprovable sentences are formally independent.
So here are my questions:
From what I’ve read, I think I understand why G is unprovable and why it must be true when interpreted with M. What I still don’t get is why does it also have to be true when interpreted about A? Could it not be the case that G is true under only the first model but not the second?
Assuming that the above question has a good answer (and I’m sure it does) does that means that assuming PA is consistent, couldn’t we mine it for arithmetical truths? We could construct a Gödel sentence and just look at it’s interpretation under A, then construct a new Gödel sentence by formalizing it a different way and that would represent another truth. I’m sure there is something fundamentally wrong with this idea but I don’t know what.
In regards to the proof predicate Prf(x, y), what exactly is that? Is it an equality like x=y (with a lot more constants I’m sure), is it an implication such as x y, or something else?
Keep in mind that I’m not a mathematician or a logician, I’m just a guy who is fascinated by logic but never learned the technical details. If you wish to reply, I’ve pasted an example I found on Peter Smith’s free online book Gödel Without (Too Many) Tears for your copying and pasting convenience:
Defn. 47 U(y) =def ∀x¬Gdl(x, y).
Now we diagonalize U, to give
G =def U(U) = ∀x¬Gdl(x,U). https://www.logicmatters.net/resources/pdfs/gwt/GWT2f.pdf (page 72)