> However, although G is undecidable, it’s clearly true.
That's... not really true; it's surprising to see it in Quanta, of all places.
Godel's (separate) completeness theorem says that in first-order logic, anything that's semantically true in all possible scenarios can be syntactically proved. So, if G is "clearly true", that ought to make it provable.
The theorems don't contradict each other because in FOL, G is not guaranteed to be true. Its truth is independent of the machinery Godel put in place.
It's not something you really need to get into an introductory text, but it actually makes the whole outcome easier to grasp, and leads to many more counterintuitive results, such as Skolem's paradox.
It’s clearly true in The Natural Numbers. It’s not provable because in some model it’s false. Being clearly true in one model does not make it provable.
Yes it is true in the unique model of second order PA, aka the computable model, aka the "standard" model.
G says: "I am not provable". As shown by Gödel, that's a true statement about G, ergo G is true. That first-order logic cannot prove it to be true is an indictment on the power of deduction, not on the truthiness of G.