Talk:Roger Penrose
|
|
Roger Penrose/Talk
I am a Roger Penrose enthusiast, but certainly not an expert on any of the topics he discusses. However, I will share a few thoughts in the hopes that those better qualified can improve the article:
I believe that Sir Penrose was not saying that humans can solve the halting problem; on the contrary, he is saying that humans can understand why the general halting problem is undecidable, while algorithms (or formal logic)cannot establish the same impossibility. This implies that there is something in human intelligence that is beyond the capability of computers. These arguments are fleshed out in Shadows of the Mind, the sequel to The Emperor's New Mind. In Shadows he phrases his arguments in terms of Godel's revolutionary theorems that describe the limits of formal logic as a foundation for mathematical truth. SRW
That would be an extremely odd claim to make. The proof of the undecidability of the halting problem is a very simple logic proof. Computer logic systems can easily check that proof. Given the axioms and the theorem, they can search and find the proof. If Penrose is saying "formal logic cannot establish the same impossibility", then he might want to read the halting problem article, where formal logic does establish the impossibility. No mathematician would have believed the result if it hadn't been proved by formal logic.
- I think you are confused between a formal logic proof and a typical human proof. Most substantial proofs are not symbolically formulated and theorem-checked by a computer, that would be hopelessly complicated. Most proofs are written in strict but not formal notation, and consensusly agreed upon by the mathematical community using their own human reasoning. Mathematicians have certainly been believing in proofs long before formal axiomatic proofs were first introduced around a century ago. --rem120
- Possibly not feasible, but not impossible. "Feasibly impossible" is a contradiction in terms. Paul Beardsell 19:41, 26 Jul 2004 (UTC)
- Yes that was badly worded, have now edited it. --rem120
My reading of Penrose differed somewhat. I saw him saying no formal logic system can solve the halting problem, but humans can, therefore humans can go beyond the power of formal logic systems. I've talked with a number of mathematicians who have read the book, and they all had the same understanding of what he was saying. If he really did make the blatant error you suggest, then we could add that to the article, but I think he made the more subtle error that I attributed to him. --LC
- My reading is that Penrose is not suggesting humans can solve the halting problem for all cases. He is simply stating that there is at least one case where humans can solve it, where no algorithm can give that same answer. This demonstrates that there must be some non-computability in human reasoning. You only need to consider this one halting problem case, not every single case. --rem120
- Maybe. But, if so, are you saying that your point has escaped the critics of Penrose's hypothesis? Paul Beardsell 19:41, 26 Jul 2004 (UTC)
- I dont think most critics of Penrose make the confusion that it is claimed that humans can solve every single halting problem case. There are many rebuttals, but this is not one of the ones I have seen Penrose bother debating. --rem120
He also made an error in his discussion of Goedel's theorem. He said that given a mathematical system of sufficient power, we could use Goedel's method to construct a statement G, which might be thought of as saying "I cannot be proved". Then, G would be unprovable within the formal system, yet we as humans would know G was true, thereby transcending the formal system.
That's incorrect. We don't know G is true. We don't know the statement "G is unprovable" is true. All we know to be true is the statement "either G is unprovable, or this system is inconsistent". That's all we know. And we can prove that within the formal system. Goedel himself proved that using ordinary logic. Maybe this should be added to the Penrose page and the page on Goedel's incompleteness theorem. It seems to be a common misconception. --LC
- I think we can prove that to prove that "either G is unprovable, or this system is inconsistent" you need meta-matematical arguments that can't be expressed within the formal system. You need to be out of the system. Joao
- The statement "either G is unprovable, or the system is inconsistent" is exactly what Goedel's incompleteness theorem proves. His proof of the theorem was no more "meta-mathematical" than any other proof. For any given system of axioms, you can construct G and prove that statement while staying entirely within the system. --LC
The ideas here are very subtle, but at the risk of seeming foolish I want to point out what seems to me to be the essential argument for conscious knowledge transcending algorithmic behavior (I think this argument is in the spirit of Penrose):
It is possible to construct a sequence of formal statements G1, G2, ? , such that within the formal system each of the statements Gn is provable for every n, but such that the higher order statement ?for every n, Gn? is not provable within the system. As humans looking from outside the formal system we can see that ?for every n, Gn? is, indeed, true (has no counterexamples), even though the formal system is not strong enough to contain a proof.
Actually, we can only know that ?for every n, Gn? is either true or the axiom system is inconsistent. But, if the axiom system is inconsistent, then every statement is true (and, every statement is false). So, it seems to me that the question of consistency is not relevant to this argument that conscious knowledge transcends algorithmic behavior.
Perhaps someone could ask a logician for clarification. SRW
There are two problems:
- the problem is that the choice is *not* between "true but
unprovable" and "inconsistent". Rather the choice is between "unprovable" and "inconsistent." There are numerous examples, where you can add a statement P to the axiom system and come up with something that is consistent and you can also add the statement not-P to the axiom system and come up with something equally consistent. In these situations, it seems pretty clear to me that being a conscious being doesn't really give you and advantage in deciding what to do.
- the other problem is that human beings can be wrong. I can know that an axiom is true. I can know that an axiom is false. True might be consistent with the axiom system. False might also be consistent with the
axiom system. I might be totally wrong. In any case, there doesn't seem anything magical about "knowing"
Can we agree that the essence of the dispute is the supposed existence of a statement P with the following properties?:
· Anyone who cares to think about it will agree that P is true.
· Neither P nor ~P is provable within an arbitrarily strong formal logic as consistent as the natural numbers. Equivalently, P is independent of the other axioms.
Clearly, Penrose has not entirely succeeded in providing an example of P, since not everyone accepts that his candidate P is true. In reverse, this reminds me of the Banach-Tarski paradox: Tarski is reputed to have been very disappointed that his theorem did not result in everyone rejecting the axiom of choice as an obviously useful (and true?) tool for the working mathematician.
This is fun; I haven't thought about these things for years. SRW
Roger Penrose is *not* saying humans can solve the halting problem for all cases. the halting problem requires the determination of halting for any given algorithm, not just one. instead he is saying there is at least one case where a human can determine whether a specific algorithm will halt, and that no algorithm could determine this. this one case shows that humans must posess some intelligence from beyond the realm of algorithmic behaviour.
Roger Penrose is *not* saying humans can know the truth of unprovable statements. these statements are provable. they are just not decidable by a formal system. proof is not equivalent to an axiomatic theorem. the statements that are claimed to be unprovable can be found in Penrose's The Emperors New Mind and Shadows Of The Mind, with their proofs.
Roger Penrose is *not* saying humans can prove the halting problem while algorithms can not. this is totally missing the point of the proof.
The fundamental semantics of Roger's work is being skewed and misinterpreted time and time again, and is costing his work a lot of credibility. It is amazing how many false statements one can read about his work in this area.
Emperors New Mind
I've rewritten the section covering the arguments in the emporers new mind, I think it was innacurate and misleading as it was, I believe it's much better now. Any thoughts? --Starx 16:05, 26 Mar 2005 (UTC)