Penrose Cannot Consistently Assert
Penrose Cannot Consistently AssertFrom MistakesOfRogerPenrose on RogerPenrose's use of GoedelsIncompletenessTheorem. See also IsFkkActuallyTrue.
Consider the statement: "Penrose cannot consistently assert this statement" (as discussed in GoedelEscherBach and attributed to CH Whitely). You can see (a) that it is true and (b) that Penrose cannot consistently assert it. So how is Penrose better off than Goedel's formal system? -- DaveHarris
I. The point is not that every formal system can be "defeated" by at least one sentence whereas people cannot. The point is that every formal system can be defeated by a specific sentence and that that particular sentence cannot defeat a mathematician who knows Goedels theorem and understands its proof. Mathematicians can have many other weaknesses including some that specific formal systems do not have, but the existence of the specific sentence proves that a mathematician cannot be identical with any element of the set of all formal systems. --MartijnMeijering
What's the relevance of "that particular sentence cannot defeat a mathematician who knows Goedels theorem and understands its proof". What does that actually mean? For any given statement, we can construct infinitely many formal systems which can understand it, just by adding it as an axiom. So that fact that humans can understand it too doesn't mean they are not formal systems; they may be just formal systems that have the axiom (or something equivalent but less naive). -- DaveHarris
Choose any specific formal system F. A mathematician can construct a Goedel sentence G_F for it. Different formal systems will generally require different Goedel sentences. G_F defeats F but does not defeat the mathematician who constructed it. This means that the indicator functions of the sets of proveable statements for the mathematician and F differ in at least one point. In other words G_F proves that the mathematician and F are not equivalent. But, by Goedel's theorem, we can repeat this argument for any formal system. In other words our mathematician is not equivalent with any of the formal systems. -- MartijnMeijering
(I deleted some stuff because it was not as clear as the above exposition (for which thanks) or (hopefully) as the stuff I am about to write. -- DaveHarris)
This rests on two ideas. First we have the belief that Penrose can construct G_F for any F. How can we be sure of this? Presumably because we know a formal procedure for doing it. It follows that this is a trick formal systems can also do. (In fact, in his book Penrose gives a formal procedure for doing this.) OK. [Technically, this is something a Turing machine can do, not a formal system. Formal systems don't do anything. --sh]
The second idea is the belief that G_F will defeat F but not Penrose. Why do we think this? We might expect that because Penrose understands Goedel and actually wrote down G_F himself, that of course he knows whether it is true. But that doesn't really follow. Consider: we're saying (in the above paragraph) that a formal system could also write down G_F; does it follow that the formal system understands Goedel and knows the truth of G_F? Presumably not. [You seem to be subtly confusing Turing machines and formal systems here. A formal system cannot "write down" its own Goedel sentence. A TM can write down the Goedel sentence of any formal system.]
The interesting case, of course, is when F=Penrose. Assume what was to be disproven, that Penrose himself is a formal system. Ask him to produce G_Penrose. He can do it; that's easy. Now ask, does G_Penrose defeat Penrose? The answer is surely that it does, by definition.
There's no contradiction here. Obviously we can't prove that Penrose is a formal system by this means, but we can say his being so does not contradict Goedel's Theorem. It really comes down to why you think "G_F ... does not defeat the mathematician who constructed it". This is discussed on IsFkkActuallyTrue. One of the ideas there is that Penrose may believe G_Penrose is true even though he cannot prove it. But if he can't prove it, he doesn't really know, he's just guessing. He could be wrong. -- DaveHarris
Your argument rests on the assumption that there actually exists a G_Penrose. I'm afraid we have to get a bit more technical to get to the bottom of this. We need to be more precise about HowGoedelSentencesWork. --MartijnMeijering
This doesn't sound very promising to me. I thought we agreed that Penrose could construct a G_F for every F. It follows he can construct G_Penrose - unless you are starting from the assumption that Penrose is not formal system. In which case you have a circular argument. -- DaveHarris
Penrose can construct G_F for every formal system F. If you already knew he was a formal system, it would follow that there exists a G_Penrose, that is a formal mathematical statement that at the face of it looks like a statement about PrimeNumbers or something like that but is in fact equivalent with the statement "this statement cannot be proved by Penrose". But this is exactly the question we're trying to answer. It would be circular to assume he is equivalent with a formal system. It would be equally circular to assume he isn't. For the time being we just don't know. We haven't proved the existence of G_Penrose, nor have we disproved it. -- MartijnMeijering
Penrose's claim is that to assume mathematicians are formal systems leads to a contradiction by way of Goedel. We seem now to be agreed that it does not, and hence that Goedel has nothing to say about about the matter. That's all I wanted to show. Penrose (as described here) has been debunked.
Are we agreed on this? It seems to me you have changed your position since you wrote the comment in the section below, about proof by contradiction. -- DaveHarris
I haven't changed my position and I don't agree Penrose has been debunked in this respect. I can show how to construct G_F. Before you can use G_Penrose in an argument you would have to show that it exists. More later. --MartijnMeijering
I've now got the ShadowsOfTheMind book. Is there a place where he considers G_Penrose or shows why he doesn't need to, that I've missed? (I have to say, I find these chapters very hard to read, so I may be missing it. Q6 starts in a promising way but vears off.) If so, you can just point it out if that will help. If not, does that mean you are consciously diverging from him? -- DaveHarris
I'm not sure what you mean by G_Penrose. Is it the statement "Penrose cannot prove this statement"? I think we can agree that this statement is true and therefore Penrose cannot prove it. But what does that prove? Not that Penrose is an algorithm. If you were able to find an algorithm that could prove this (bloody hard, I imagine, an absolute proof about the real world), that would show that Penrose was at least different from that particular algorithm.
With Fk(k), the situation is different. It is a statement about numbers, not about proveability of theorems. Due to its ingenious construction it is logically equivalent with such a statement however. -- MartijnMeijering
By G_Penrose I mean the Goedel sentence for the formal system that is Penrose. It will be a long piece of mathematics. It is exactly Fk(k) where the formal system is Penrose. -- DaveHarris
This presupposes that Penrose is a formal system. How would we go about constructing G_Penrose? If we already had the precise algorithm, it would be easy, but then why bother if we already know he is an algorithm? --MartijnMeijering
It is quite possible that humans use "informal" systems. Nothing asserts that humans use formal mathematical systems. I question the applicability of Goedel's proof to humans.
So do I. But it is only used in a proof by contradiction. If we assume, for the sake of argument, that Goedel's theorem applies to humans, this leads to a contradiction. Therefore we conclude that we cannot apply Goedel's theorem to humans and consequently that humans are not (completely) equivalent with algorithms. --MartijnMeijering
Yes. As Penrose puts it, "My use of the Goedel argument is to show that human understanding cannot be an algorithmic activity" (ShadowsOfTheMind p51). If you never rated the possibility that it was maybe the formal proof won't add much. Unless you like to watch the philosophical sparks fly that is. -- RichardDrake
Yes, too. I don't know whether humans are, in fact, formal systems, and I don't much care. Maybe they are not; maybe they do run on quantum effects. Penrose's claim is much stronger than that, much more scary: he says they can only run on non-formal principles. They cannot even be emulated by Turing Machines. -- DaveHarris
That assumes that a Turing Machine cannot emulate an "informal system". That's not clear to me at all; what is shown is that they can "emulate" a formal system. But the fact that they can emulate a formal system does in no way say anything anout their ability to emulate informal systems. Whatever an informal system might be. (probably some fuzzy-logic system?)
As an aside, I put "emulate" between quotes because there's really nothing to emulate avbout a formal system; a formal system doesn't do anything, it just is. On the other hand, humans and Turing Machines do things; one of the things Turing Machines can do is to enumerate all propositions that are true in a formal system (I suppose that is meant by "emulating" a formal system). One thing both can do is, given a formal system, construct its Goedel sentence Fk(k). Another thing both can do is to write down this Goedel sentence Fk(k) followed by the words "is obviously true according to my deep mathematical insight".
Here's another angle which may (or may not) help. I should mention that I sometimes think of formal systems as being computer programs, so it's easy to imagine having a conversation with them. This can be made more rigorous if need be. [You should watch out; despite the fact that there is a strong relation between formal systems and computer programs, they are by no means equal. In particular, a computer program P exists that takes as input a formal system and outputs its Goedel sentence. Say we give P a formal system F as input. We can model the working of P in F. We can then prove in F the following proposition: "program P produces G_F on input F". This theorem is distinct from G_F! Despite the fact that P can produce G_F, and F can model the working of P, G_F is not a theorem in F. --sh]
Suppose G_Penrose exists and Penrose claims to understand it even though he can't prove it. Let's believe him: he has some non-formal mechanism for understanding G_Penrose, divine inspiration say. Now suppose we have a formal system that also claims to understand its own Goedel sentence. Why shouldn't we believe the formal system, too? Why can't formal systems get divine inspiration? What is the basis for treating the formal system any differently to how we treat Penrose? -- DaveHarris
Some points:
Here's another attempt... Penrose believes G_Penrose is true because he reasons as follows:
What do we mean by "G_F is true"? As far as I can tell, we mean G_F can be proven by some other formal system F', where F' is in some sense bigger than F. So Penrose knows that G_Penrose can be proven by some formal system Penrose'. Penrose cannot prove G_Penrose himself; he just knows the proof is possible for other people, therefore he believes it.
I think there is room for dispute over whether this reasoning is sound. More importantly, I don't see why a formal system shouldn't reason the same way - erroneously or not. -- DaveHarris
I don't think the reasoning above is how Penrose reasons. He is unconcerned with the truth of G_Penrose, whatever that is. He would probably agree that it is true, but, because of it's catch-22 nature, he is unable to prove it. --MartijnMeijering
Just one question: given a sentence, X, how for a formal system (or Penrose) determine that that sentence is its G_F? There are many sentences that Penrose assumes to be true but cannot prove (This is true of every human being): If he could tell us which of these was his G_Penrose then perhaps we could get somewhere. Unfortunately, Goedel implies that no formal system can know its G_F. If it did, then it would know it was true. --DaveWhipp
There is a formal mechanism for creating a specific G_F from a description of F, and given F and G_F it is straightforward to verify the relationship between them. I am not sure what you mean by "know", but I think a formal system can know that a given string is its G_F yet cannot know that the G_F is true. This implies that (1) cannot be proved by a formal system, nor adopted as an axiom into a formal system, etc. -- DaveHarris
If the system "knows" (i..e can prove to be true) Goedel then it knows that its G_F is true. If it can also prove that a specific sentence is its G_F then it has proven (Modus Ponens) that its G_F is true. But Goedel proves that no system can prove that its G_F is true, so no system can prove that Goedel is true and also that a given sentence is its G_F.
Imagine this computer program: it accepts an input program and tells you if it halts
bool doesItHalt(string in) {
if (isAprogramThatHaltsButIcantProveIt(in))
{
return true;
}
else if (isAprogramThatDoesntHaltButIcantProveIt(in))
{
return false;
}
else
{
return resultOfProof(in);
}
}
Such a program is plainly absurd!
By the way, the word "bigger" is wrong in that although F' can prove things which F cannot, F may be able to prove things which F' cannot.
This is a criticism I have of the dialogue in $3.23. The robot is obsessed by the idea that the scientist knows things which it cannot prove; it doesn't like to feel inferior. However, it also knows things which the scientist does not. It has no reason to feel inferior, they are at worst equal. The robot should analyse the scientist, deduce the formal rules he runs by, and derive G_Scientist. Then the robot will know something it can be sure the scientist will never catch up to. -- DaveHarris
As a complete digression, does FuzzyLogic bypass this issue entirely? In the same way that it does with the Cretan liar paradox and Set of All Sets that do not contain themselves paradox?
Is FuzzyLogic an algorithm implemented in a formal system? It is. Therefore it is limited by the limitations of the formal system.
Dave and Martijn have done very well so far here. To address one point made by Martijn above, Goedel's construction of his sentence is a proof of his theory, but nowhere does Goedel suggest that only the one construction technique is sufficient for the theory. Goedel only says that no formal system is both consistent and complete. The sentence, PenroseCannotConsistentlyAssert demonstrates that Penrose is not both consistent and complete, so it's sufficient to show Penrose isn't distinct from a formal system in a Goedelian sense. Of course Penrose may still demonstrate his superiority to formal systems in some other sense.
Most of the argument depends on the assumption that "the Goedel sentence for system F" is meaningful. It is not, there are many Goedel sentences. Constructing them is possible in more than one way, I'd assume in countably infinitely many ways. Come to think about it, just put a function in it somewhere that throws its argument away and you can add any argument you want to get infinitely many Goedel sentences.
Back to Penrose. If you construct G_Penrose and hand it to him, he'd just say "oh, this might be my Goedel sentence!", quickly derive it himself, compare it, then claim it was true. If you hand him a different G_Penrose', this will fail. He has to derive all possible Goedel sentences until he hits the right one. He cannot answer as long as he didn't hit it.
It seems, there are far more ways to construct G that Penrose could reproduce. (Admittedly, this is just my gut feeling about the incompleteness theorem and turing machines in general: There's always more than you could enumerate.) Since we know how he's going to enumerate the possibilities, we can choose a different one. He'll never know about it. Penrose is still omega-incomplete.
One should also keep in mind that Penrose may be a complete, though inconsistent system. That would allow him to prove his own Goedel sentence and then write a book about it full of utter nonsense :)
Another problem, besides Penrose's lack of consistency (which is somewhat shown by his failure to accept that the lack of human consistency is an alternative solution to the problem that seems to make somewhat more sense, in an OccamsRazor kind-of way) is this: In order to prove that G_penrose is true, Penrose must know F_penrose (in order to compare it using the method of constructing G). However, the mere act of knowing his own formal system would actually modify that formal system, so the system performing the proof would not be the same one for which the sentence is the Goedel sentence. -- JulesH
EditText of this page
(last edited March 8, 2011)
or FindPage with title or text search