We know that the problem of deciding if a program halts on some input is undecidable via computation.

But suppose we have a partial program P(C,I), to decide halting/not-halting of a program P on an input I, with errors, including input not being of right type, counting as a halt.

For instance, P sees a loop at the start of the program for which there is no exit or it sees that the program is trying to find a prime which ends with 4. It marks these cases as non-halting. Halting cases can always be marked by P as halting by just running the code in one thread and waiting to see if it halts. The third option, non-halting programs which are not seen to be so, in this case P itself runs forever.

Now given P, it is possible to construct P' a program which detects all the non-halting programs that P does, but atleast one more non-halting case also. To do this consider R, with R(C)=not(P(C,C)) which takes an input program C, asks P 'does C halt with input the source of C itself'. Then R reverses P's decision. If P says halt, then R does not halt on C. If P says not-halt, R halts and finally if P is undecided(so P doesn't stop), R again doesn't halt.

What about R(R), R applied to itself. P(R,R) can't be decisive as we will get a contradiction. But in fact R(R) doesn't halt, as all halts are detected by P.

So, P' is basically P with the extra detection - R(R) doesn't halt.

This proves the weaker claim of Penrose

'No knowably correct program P, can simulate human behaviour' as we can see that if P is right, P' is also right.

The 'knowably correct' might seem like an escape hatch, but it is actually hard to split the difference. Simulating humans necessarily means simulating a group of humans who are also doing verification of their initial results with each other and proof-assistants.

Also, going from P to P' is a computable process, but if you try to add this to P, you get a new program with a new limitation.