The mistake that you are making is to imagine that I must be making a mistake.
Let's take a few examples.
He claims that a robot which is able to engage in Gödelian reasoning, cannot possibly be computable. Logicians agree that this claim is false. Indeed https://link.springer.com/article/10.1007/s10817-021-09599-8 shows a version of Gödel's theorem that has been fully checked via proof assistant. While we still lack AIs that are able to produce such proofs (other than by regurgitating such proofs in their input data), in principle a proof checker filtering the output of a brute force search through possible proof attempts will achieve any possible machine checked proofs. But proof checkers can proof check Gödelian reasoning. Thus we already know how to write a (rather impracticable) robot that does exactly what Penrose claims to be impossible.
Here's a whopper. Let's go to this passage from 4.2 of his rebuttal.
However, I had been disturbed by the possibility that there might be true mathematical propositions that were in principle inaccessible to human reason. Upon learning the true form of Gödel's theorem (in the way that Steen presented it), I was enormously gratified to hear that it asserted no such thing; for it established, instead, that the powers of human reason could not be limited to any accepted preassigned system of formalized rules. What Gödel showed was how to transcend any such system of rules, so long as those rules could themselves be trusted.
This is complete and utter bullshit. Gödel did not show that we could transcend any such system of rules. What Gödel demonstrated is what those rules can prove of themselves. Namely, "If this set of axioms proves itself consistent, then it is inconsistent." Which statement can be proven using nothing more than arithmetic. Our ability to prove this doesn't prove that our mathematical reasoning is somehow beyond what a mere formal system can prove. It is just a demonstration that we can follow a piece of arithmetic to its logical conclusion. Any other understanding of the result is simply a mistake.
He's also wrong about whether there are problems that, in principle, are beyond human reason. For example consider the BB(n) problem. Identifying which Turing machine gives us BB(643) is impossible from ZFC. (See https://github.com/CatsAreFluffy/metamath-turing-machines for more.) If you go to BB(1000), no set of axioms that mathematics has ever debated can suffice. Going beyond human comprehension doesn't take much more than that.
Of course those are weak estimates. In fact it is likely that BB(10) is going to be forever beyond us. And no, some magic quantum decoherence in the microtubules isn't going to fix that.
Let's move on. Section 4.5. He admits to the logical possibility that he is wrong, then asks whether unsoundness is plausible. How is it not plausible? The only form of intelligence that we have an existence proof for, us, thinks in notoriously unreliable ways. LLMs are our best attempt to replicate our verbal abilities by computers. They are likewise extremely unsound.
The burden of proof that soundness is possible here is on Penrose. And he needs to prove it soundly enough to overturn the generally accepted conclusion that the known laws of physics suffices, in principle, to explain the manner by which our brains operate. Because that is the conclusion that he is aiming to convince people of.
He doesn't even try. He waves his hands, declares absurdity, and moves on. That may be fine from the point of view of his philosophy. It is not fine from the point of view of a logician. It's a gap. And a mighty big one at that.
I could go on, but what's the point? If you refuse to believe what logicians say about logic, then no explanation of what logicians have to say will convince you. And if you do believe what logicians say about logic, then you should already know that Penrose is wrong.
As Penrose points out, the claim is conditional. Take a recursively axiomatized theory T for which we have Pi_1 soundness level warrant, i.e., we have reason to think its Pi_1 theorems are true in the standard model N for the arithmetical cases we care about. Then we can see (again: in N) that G_T is true while T cannot prove it.
That gives principled grounds to adopt Pi_1 reflection or otherwise step to a stronger T'. No infallibility claim about people is require. This mirrors the ordinary kind of warrant mathematicians use when they adopt new axioms after scrutiny and debate.
>A proof checker plus brute-force search can do Gödel reasoning, so a robot can do it.
A checker plus search enumerates exactly the theorems of whatever fixed system it’s tied to. You can also script computable progressions that iterate reflection or consistency along recursive ordinal notations in the Turing/Feferman style. That’s still a single computable progression determined in advance. It isn’t that such progressions don’t exist, but that our justified acceptance is not a priori bounded by any one fixed computable progression.
The mechanist reply here is an existence thesis: there exists some computable procedure whose output matches everything humans could in principle come to rightly endorse for arithmetic. If that’s your view, give the existence argument. If instead you propose a specific computable progression P that we could in principle ratify as Pi_1 sound in toto, Gödel/reflection immediately pushes past P. If you say we can’t justifiably ratify P as a whole, you’ve conceded the point that no single precommitted computable scheme captures the moving boundary of what we’re warranted to accept.
>Gödel didn’t show transcendence.
In the narrow sense above, Gödel shows how to go beyond any accepted, fixed rule set once we have Pi_1 soundness level warrant for it. That is exactly the move at issue. Note the scope: inside a system you can’t adopt “if provable then true” without collapse by Löb. Outside, adopting restricted Pi_1 reflection is the justified step. If you want to reject the move, reject the warrant. Deny that we sometimes justifiably regard a given fragment of T as Pi_1 sound for the cases at hand. That’s an objection about epistemic warrant, not a logic gotcha.
>Busy Beaver shows limits, so case closed.
Busy Beaver actually helps here. It yields concrete Sigma_1 statements that can be independent of strong base theories, illustrating that warrant-driven extensions are sometimes needed to settle specific instances.
Either sometimes we do have adequate Pi_1 level meta warrant for a theory T on the arithmetical claims we care about. In which case we can recognize G_T as true in N and rightly move to T', ensuring our recognitions outrun that fixed T. Or deny such warrant altogether, in which case you haven’t refuted the conditional. You’ve just changed the target to a weaker notion of “what we can recognize.” The “humans are unsound” line doesn’t touch that conditional, and “just use a checker plus search” doesn’t answer the challenge unless you can support the existence of a single computable theory or precommitted progression that captures everything we could in principle come to rightly accept for arithmetic.
Let's take a few examples.
He claims that a robot which is able to engage in Gödelian reasoning, cannot possibly be computable. Logicians agree that this claim is false. Indeed https://link.springer.com/article/10.1007/s10817-021-09599-8 shows a version of Gödel's theorem that has been fully checked via proof assistant. While we still lack AIs that are able to produce such proofs (other than by regurgitating such proofs in their input data), in principle a proof checker filtering the output of a brute force search through possible proof attempts will achieve any possible machine checked proofs. But proof checkers can proof check Gödelian reasoning. Thus we already know how to write a (rather impracticable) robot that does exactly what Penrose claims to be impossible.
Here's a whopper. Let's go to this passage from 4.2 of his rebuttal.
However, I had been disturbed by the possibility that there might be true mathematical propositions that were in principle inaccessible to human reason. Upon learning the true form of Gödel's theorem (in the way that Steen presented it), I was enormously gratified to hear that it asserted no such thing; for it established, instead, that the powers of human reason could not be limited to any accepted preassigned system of formalized rules. What Gödel showed was how to transcend any such system of rules, so long as those rules could themselves be trusted.
This is complete and utter bullshit. Gödel did not show that we could transcend any such system of rules. What Gödel demonstrated is what those rules can prove of themselves. Namely, "If this set of axioms proves itself consistent, then it is inconsistent." Which statement can be proven using nothing more than arithmetic. Our ability to prove this doesn't prove that our mathematical reasoning is somehow beyond what a mere formal system can prove. It is just a demonstration that we can follow a piece of arithmetic to its logical conclusion. Any other understanding of the result is simply a mistake.
He's also wrong about whether there are problems that, in principle, are beyond human reason. For example consider the BB(n) problem. Identifying which Turing machine gives us BB(643) is impossible from ZFC. (See https://github.com/CatsAreFluffy/metamath-turing-machines for more.) If you go to BB(1000), no set of axioms that mathematics has ever debated can suffice. Going beyond human comprehension doesn't take much more than that.
Of course those are weak estimates. In fact it is likely that BB(10) is going to be forever beyond us. And no, some magic quantum decoherence in the microtubules isn't going to fix that.
Let's move on. Section 4.5. He admits to the logical possibility that he is wrong, then asks whether unsoundness is plausible. How is it not plausible? The only form of intelligence that we have an existence proof for, us, thinks in notoriously unreliable ways. LLMs are our best attempt to replicate our verbal abilities by computers. They are likewise extremely unsound.
The burden of proof that soundness is possible here is on Penrose. And he needs to prove it soundly enough to overturn the generally accepted conclusion that the known laws of physics suffices, in principle, to explain the manner by which our brains operate. Because that is the conclusion that he is aiming to convince people of.
He doesn't even try. He waves his hands, declares absurdity, and moves on. That may be fine from the point of view of his philosophy. It is not fine from the point of view of a logician. It's a gap. And a mighty big one at that.
I could go on, but what's the point? If you refuse to believe what logicians say about logic, then no explanation of what logicians have to say will convince you. And if you do believe what logicians say about logic, then you should already know that Penrose is wrong.