Right, so definitely check Aaronson, the entirety of what I linked is a couple dozen pages at most. But the statement you quoted, while true, is deliberately p

Right, so definitely check Aaronson, the entirety of what I linked is a couple dozen pages at most. But the statement you quoted, while true, is deliberately provocative. There are two standard statements: - The one for the First Incompleteness Theorem implies the existence of a statement P independent from the theory, i.e. one that can be neither proved nor disproved using it. (That is, theory proves false iff theory + P proves false iff theory + not-P proves false.) Here we don’t opine on whether P is true or not. - The one for the Second Incompleteness Theorem points to a specific statement: the consistency of the theory (that you can state that within the theory itself is nontrivial, but at the same time much of the point of and the reason for the whole hubbub). Here we know it’s true because we assumed it! That is, in the metalogic which we’re (implicitly, unless you dive in very deep) using to reason about all this, we have the disjunction: - Either the theory proves false, then it proves anything at all (boring); - Or it does not prove false, then it does not prove th(e true statement th)at it does not prove false. Why we can’t just cut out self-referential stuff in our logic... for the same reason we can’t (usefully) just cut out infinite loops in our programming language, I think: it doesn’t take much to have either of those. The statements are not self-referential in any exotic way. What you need is—AFAIU—for the theory to be able to be able to talk about (at least in terms of halting or not) programs in a Turing-complete language, a proof verifier for the theory written in that language and an interpreter for itself in it. Encoding all of that in Peano arithmetic is predictably awful (especially if your name is Gödel, you have never seen a programming language, and Turing completeness hasn’t been invented yet). But none of it is exactly advanced functionality for a logic system; the self-interpreter isn’t even a part of it, it’s just something all Turing-complete languages can do. (This part is more wishy-washy than I’d like, but that’s what you get for asking an amateur.)