[funktour]

(for the record, I think the Penrose take on Gödel and consciousness is mostly silly and or confused)

I think your understanding of the incompleteness theorem is a little, well, incomplete. The proof of the theorem does involve, essentially, figuring out how to write down "this statement is not provable" and using liar-paradox-type-reasoning to show that it is neither provable nor disprovable.

But the incompleteness theorem itself is not the liar paradox. Rather, it shows that any (consistent) system rich enough to express arithmetic cannot prove or disprove all statements. There are things in the gaps. Gödel's proof gives one example ("this statement is not provable") but there are others of very different flavors. The standard one is consistency (e.g. Peano arithemtic alone cannot prove the consistency of Peano arithmetic, you need more, like much stronger induction; ZFC cannot prove the consistency of ZFC, you need more, like a large cardinal).

And this very much does come up for real systems, in the following way. If we could prove or disprove each statement in PA, then we could also solve the halting problem! For the same reason there's no general way to tell whether each statement of PA has a proof, there's no general way to tell whether each program will halt on a given input.

[Chance-Device]

Nice reply. I don’t know anything about Peano arithmetic, or how it applies to the halting problem, so I can’t really evaluate this. All I know is the description of the proof that I read some time ago. Maybe there’s more to dig into on it, but as you say at the start of your post, likely none of it has anything to do with what Penrose is arguing for.