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.

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

---

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