He misrepresents Penrose's argument. I remember Scott Aaronson met Penrose later on, and there was a clarification though they still dont agree.
In any case, here's a response to the questions (some responses are links to other comments in this page).
> Why does the computer have to work within a fixed formal system F?
The hypothesis is that we are starting with some fixed program which is assumed to be able to simulate human reasoning(just like starting with the largest prime assuming that there are finitely many primes in order to show that there are infinitely many primes). Of course, one can augment it to make it more powerful and this augmentation is in fact, how we show that the original system is limited.
Note that even a self-improving AI is itself a fixed process. We apply the reasoning on this program including its improvisation capability.
This argument would fall apart if we could simulate a human mind, and there are good reasons to think we could. Human brains and their biological neurons are part of the physical world, they obey the laws of physics and operate in a predictable manner. We can replicate them in computer simulations, and we already have although not on the scale of human minds (see [1]).
It's on Penrose and dualists to show why simulated neurons would act differently than their physical counterparts. Hand-waving about supposed quantum processes in the brain is not enough, as even quantum processes could be emulated. So far, all seems to indicate that accurate models of biological neurons behave like we expect them too.
It stands to reason then, that if a human mind can be simulated, computers are capable of thought too.
Hand-waving is not required as one is not going into microfoundations at all in the original argument. Someone making a thermodynamic argument for some conclusion, can later on try to speculate about how the conclusion is implemented with statistical mechanics. But the original argument is itself independent. Similarly, Penrose speculates about Orch-OR(which is not dualism btw, Penrose is a physicalist), but the truth of the argument isn't dependent on Orch-OR itself.
The first question is not the question I'd like answered. What I want to know is this:
> Why does the computer have to work within a CONSISTENT formal system F?
Humans are allowed to make mistakes (i.e., be inconsistent). If we don't give the computer the same benefit, you don't need Godel's theorem to show that the human is more capable than the computer: it is so by construction.
Take a group of humans who each make observations and deductions, possibly faulty. Then, they do extensive checking of their conclusions by interacting with humans and computer proof assistants etc. Let us name this process as HC.
A program which can simulate individual humans should also be able to simulate HC - ie. generate proofs which are accepted by HC.
---
Penrose's conclusion in the book is more weak - that a knowably correct process cannot simulate humans.
We now have LLMs which hallucinate etc that are not knowably correct. But, after reasoning based methods, they can try to check their output and arrive at better conclusions, as is happening currently in popular models. This is fine, and is allowed by Penrose's argument. The argument is applied to the 'generate, check, correct' process as a whole.
(I don't see how that relates to Godel's theorem, tough. If that's the current position held by Penrose, I don't disagree with him. But seeing the post's video makes me believe Penrose still stands behind the original argument involving Godel's theorem, so I don't know what to say...)
That a knowably correct program cant simulate human reasoning is basically Godel's theorem. One can use a diagonalization argument similar to Godel's proof for programs which try to deciding which Turing machines halt. Given a program P which is partially applicable, but always correct, we can use diagonalization to construct P' a more widely applicable and correct program ie. P' can say that some Turing machine will not halt while P is undecided. P'. So, this doesn't involve any logic or formal systems, but it is more general - Godel's result is a special case as the fact that a Turing machine halts can be encoded as a theorem and provability in a formal system can be encoded as a Turing machine.
Penrose indeed, believes both in the stronger claim - a program can't simulate humans and the weaker claim, a knowably correct program can't simulate humans.
The weaker claim being unassailable firstly shows that most of the usual objections are not valid and secondly, it is hard to split the difference ie. to generate the output of HC using a program which is not knowably correct. A program whose binary is uninterpretably but by magic only generates true theorems. Current AI systems including LLMs don't even come close.
In any case, here's a response to the questions (some responses are links to other comments in this page).
> Why does the computer have to work within a fixed formal system F?
The hypothesis is that we are starting with some fixed program which is assumed to be able to simulate human reasoning(just like starting with the largest prime assuming that there are finitely many primes in order to show that there are infinitely many primes). Of course, one can augment it to make it more powerful and this augmentation is in fact, how we show that the original system is limited.
Note that even a self-improving AI is itself a fixed process. We apply the reasoning on this program including its improvisation capability.
> Can humans "see" the truth of G(F)?
https://news.ycombinator.com/item?id=43238449
> one only has to note that even if you believe humans can "see" truth, it's undeniable that sometimes humans can also "see" things that are not true
https://news.ycombinator.com/item?id=43238417