The Penrose–Lucas argument

I was looking at the Penrose–Lucas argument as discussed on Wikipedia. It states:

In 1931, the mathematician and logician Kurt Gödel proved that any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete. Further to that, for any consistent formal theory that proves certain basic arithmetic truths, there is an arithmetical statement that is true, but not provable in the theory.

In his first book on consciousness, The Emperor's New Mind (1989), Penrose made Gödel's theorem the basis of what quickly became an intensely controversial claim. He argued that while a formal proof system cannot, because of the theorem, prove its own incompleteness, Gödel-type results are provable by human mathematicians. He takes this disparity to mean that human mathematicians are not describable as formal proof systems, and are not therefore running an algorithm.

If find this hard to believe, because I can't see why either one of the following is true:

(1) Humans are proving incompleteness not using the system itself, but using some greater system
OR
(2) If there is a proof of incompleteness that was found in the system by a human, then as long as that proof is of finite length, it could be found algorithmically simply by trying and checking every proof until one finds one which is correct.

I looked at the criticisms on the Wikipedia page, and they only criticised the science of quantum effects in the brain, not the mathematics of the original assertion.

I'm sure I'm missing something, but is his original assertion correct? And if so, could you explain why?

-
I think this question would be better suited for Philosophy.SE – Sniper Clown Jul 2 '12 at 3:05
Mahmud: I'm more interested in the mathematics behind the statement, as in whether certain proofs can not be generated by an algorithm. I believe that's purely a mathematical question, not a philosophy one. – Clinton Jul 2 '12 at 3:17
Of course it is not correct. One can program a computer to prove Gödel-type results. – André Nicolas Jul 2 '12 at 3:57
I heard Penrose speak about this back around the time the book came out, and I thought he was misunderstanding the mathematics badly, and for essentially the reasons you give. – Gerry Myerson Jul 2 '12 at 3:57

In (belated) response to your two points more specifically:

1) I suppose the point is that humans are somehow able to identify their own formalisation, F, which they are then able to form a Godel sentence G(F) from. They can't use a greater (or lesser) system than the one they are using.

2) The incompleteness theorems don't provide a formal proof of incompleteness, per se. If they did then your argument would follow. They provide an argument of incompleteness that sits 'outside' the formalism under inspection. The Godel sentence G(F) is constructed to be true but not provable by F. It's true that this doesn't mean that another formal system, H, couldn't prove the statement G(F). But we're concerned in particular with the system F and whether it really captures our conscious reasoning.

You can read more on the IEP:

http://www.iep.utm.edu/lp-argue/#H3

-
More specifically, the theory whose only axiom is G(F) is able to prove G(F). – Asaf Karagila Feb 28 at 18:36

Shapiro (in Philosophia Mathematica (III) 14 (2006), 262–264) published a review of Torkel's book, here referred to by Gerry Myerson:

Of course, some alleged applications and consequences of incompleteness cannot be dismissed as easily as this. The Lucas-Penrose thesis (or theses) do not seem to turn on such elementary misunderstandings of what the incompleteness theorems say. Lucas and Penrose themselves certainly understand the mathematics. The author’s treatment of the issue provides a nice introduction to the underlying issues, but the book does not contain many references to the extensive literature on this topic.

I suspect that most readers of this journal do not need this book. Those who engage in contemporary debates concerning the philosophy of mathematics knowfull well what the incompleteness theorems say and what they do not say." (bold letters are mine)

That the book of Torkel falls short in addresing this issue, is quite clear. Now, to say that the problem concerns exclusively to math, confines math to a kind of closed crystal box because there are major issues in cog-sciences regarding math and logical knowledge to be explained. It might be due to phenomena such as this one here raised by Penrose and others, that social sciences in general seem so chaotic and underdeveloped in comparison to math, physics, chemistry and other comparable fields of research.

The last point I wish to bring to your attention here is the one that Clinton himself acknowledges:

(1) Humans are proving incompleteness not using the system itself, but using some greater system.

If this is true, then how exactly functions our mind or brain to be able to prove such a thing ever from a greater system?

-

I recommend Torkel Franzen's book, Godel's Theorem, for pretty much anything concerning popular misconceptions, but in particular there is a discussion of Penrose, pages 119 to 124.

-