3 ms·
> You just can't tell if it is true. But in the Penrose argument, we can start from a true system and use reflection to arrive at another true statement which
by enugu 2y ago
> You just can't tell if it is true.
But in the Penrose argument, we can start from a true system and use reflection to arrive at another true statement which is not deducible from the original system.
This is important to the argument as one starts with a proposed program which can perform mathematical reasoning correctly and is not just a random generator. Then, the inability to see the new statement is a genuine limitation.
- drivebyhooting 2y agoHow can you see something is true without proving it is true? Many an obvious truth turns out to be mendacious. See various counter examples in analysis.
- enugu 2y agoThere is no special insight required here. Merely, a simple diagonalization argument (https://news.ycombinator.com/item?id=43257904 https://news.ycombinator.com/item?id=43257904) which given a partial process to detect if a Turing machine halts, constructs a new machine which does not halt but was not detected by the earlier process.
- Lerc 2y agoWhat exactly is meant by 'use reflection'? How is it something that a computer cannot do? It seems to be just convincing yourself. Gödel's theorum itself does not help you here because you are trying to identify a undecidable but true. Gödel only showed that there are undecidable true statements, not what they are.
- enugu 2y agoGodel 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).