Godel explicitly constructs the statements (which are essentially encoding a particular self-referential statement into logic). Penrose makes this more concrete

Godel explicitly constructs the statements (which are essentially encoding a particular self-referential statement into logic). Penrose makes this more concrete where given an accurate, but necessarily partial procedure for detecting when a program halts, one can use diagonalization to show that a program wont halt even though the earlier process couldn't detect it. https://news.ycombinator.com/item?id=43257904 https://news.ycombinator.com/item?id=43257904 This construction is something that a computer can do, but not the original system itself. Once you augment the system, there is now a new statement it cant see and so on. (so on, here involves ordinals).