What exactly is wrong with this argument (Lucas-Penrose fallacy) Argument
"For every computer system, there is a sentence which is undecidable for the computer, but the human sees that it is true, therefore proving the sentence via some non-algorithmic method."
 A: The basic fallacy here comes by regarding the original Gödelian proof. First, one assumes the consistency of a theory T, and from T shows that the sentence G is undecidable. Now, to show (formally) that G is nonetheless true in the standard model (there are models in which G is false!), one requires a more powerful theory P. Now, a human can see that G is true in the same way. So, the correct statement is: G is undecidable in T, but can be shown with P to be true in the standard model. Thus the need for a non-algorithmic method is not shown so far. Further: the assumption that a human would be able to decide every sentence is an unwarranted assumption. It is not too difficult to imagine that the human will also be stumped at one point. Indeed, there are undecidable sentences for which there is no standard model, and so no "correct" decision until you add some more axioms: the mathematical literature is full of them. The most infamous one is: can a human decide the Continuum Hypothesis on the basis of the standard ZFC axioms? No. Here the human and the computer are on equal footing. (I am being a little loose here with the Church-Turing thesis in my interchanging mathematical proof with computability, but one could clean up the argument to do without it. For example, see https://math.stanford.edu/~feferman/papers/penrose.pdf)
