Lucas himself foresaw the 'expand the axioms' response, and pointed out that once you do this, you get a new formal system with a new Gödel sentence. This mean

Lucas himself foresaw the 'expand the axioms' response, and pointed out that once you do this, you get a new formal system with a new Gödel sentence. This means that no such argument against his thesis - i.e. by adding the truth of the formal system's Gödel sentence to that system's axioms - will terminate. Note that I am not saying the Lucas-Penrose argument is indefeasible; I am saying that it cannot be defeated simply by the argument that goes 1) it claims the human mind is consistent; 2) we can see that the human mind is not consistent; ergo, it is false. This argument fails because premise 1 is false. If it were this simple, the video here would not be nearly two hours long! Addendum: The "stepping out" argument is not a matter of adding axioms, it is a sort of meta-argument that a Gödel sentence for a consistent system must be true[1], and the consistency of the hypothetical system under discussion follows via the Church-Turing thesis (which you could challenge if you want to, but I suspect that, to most people who understand the implications of doing so, this would be an undesirable trade of one implausibility for another.) This leaves me wondering if the Lucas-Penrose argument can be challenged on the grounds that the algorithm in question probably does not halt (other than for causes outside the system; namely, the causes of death or the causes of a power outage), or that the question of its halting is undecidable. I am sure this response has been debated somewhere, if it is not obviously wrong. [1] https://math.stackexchange.com/questions/1491061/paradoxhow-can-godel-prove-that-godel-sentence-is-unprovable-but-true-if-such https://math.stackexchange.com/questions/1491061/paradoxhow-...