So, Roger Penrose is a bright guy, I mean, he won the Nobel Prize, but the Penrose-Lucas argument that the human mind is a hypercomputer based on Gödel's Second Incompleteness Theorem is laughably bad. For a start, it's not really that original. I think the reason the Second Incompleteness freaks out a lot of people, to the point that they claim mathematics is a kind of fantasy based on it, is they come up with a vague version of this argument on their own. I certainly did in high school.
Gödel's Second Incompleteness Theorem states that any computable, consistent formal system capable of doing arithmetic cannot prove its own consistency. Penrose says the brain is a formal system, it's consistent, it believes it's consistent, so it can't be computable. But you can only make that inference when you're unfamiliar with the details of the proof of the Second Incompleteness Theorem.
When we talk about a system proving its own consistency, at a high level, it means it encodes itself into the objects it considers in a way that plays nicely with its deductive rules, to the point that it is capable of giving a complete description of those rules in itself, and stating that that set of rules does not lead to any contradictions. I don't know the complete rules of my mind's deductive system. I know I accept ZFC, its consistency, its consistency's consistency, some large cardinals, but I don't know if there's nothing else I could add to that list. I just have this term in my formal language that refers to my formal system, and I can state some things about it, but I don't know the rules it corresponds to at the level of the Incompleteness Theorems, so it's fine. Similarly, I have this pronoun "me" that I call myself, but that's not the same as having a description of the state of every particle that constitutes me.
Furthermore, Gödel's Incompleteness Theorems don't really need computability. Just some regime capable describing itself. So we're led to the crossroads that we either can't describe the mind, or a modified Second Theorem (really, you could make the case based on Gödel sentences in the original proof of the First or via the Halting Problem) where we can't know everything detail about it within that description.
It strikes me as incredibly strange that Penrose would have stuck to his guns for so long on this. It's easy for me to see the cause of his mistake, he's not a logician and a naive understanding can easily lead one astray on this issue. But despite air-tight criticism from people who know the subject much better, he's stayed on. So I want to know if he's ever engaged with criticism on this front, or just ignored it, because the verdict is essentially universal that his argument is invalid even allowing its premises. If he has acknowledged it, why hasn't he budged?
