> However, although G is undecidable, it’s clearly true.<p>That's... not really true; it's surprising to see it in Quanta, of all places.<p>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.<p>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.<p>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.