Wednesday, 20 February 2013

Strong AI: The Gödel Problem

In my previous post, I alluded to an argument made by John Lucas and popularised by Roger Penrose against the possibility of AI, and this is that Gödel's Incompleteness Theorems suggest that even weak AI is impossible. We could never make a computer system that behaved intelligently.

Loosely put, Gödel's Incompleteness Theorems put fundamental limits on what can be achieved by working with formal systems.

In particular, some argue that they show that formal systems can never be as intelligent as human beings. In this post, I argue against this view and propose that humans are subject to the same limitations.


The Lucas/Penrose argument

Any system comprising a syntax and the available operations that may be applied to statements is called a formal system. Arithmetic is one such system. It describes how we may express statements about numbers and what operations we can perform to get from one true statement to another (e.g. divide both sides of an equation by the same amount).

There are a number of interesting results from these theorems, but most importantly for our purposes, Gödel proved that either these systems are inconsistent (e.g. can prove mutually exclusive alternatives) or there would be statements expressed in the language of these systems which are true but which could never be proven within the rules of these systems.

The way he did this is ingenious and complex, and I don't pretend to fully understand it. It can be explained in terms of a trick similar to the well-known liar's paradox - "this sentence is a lie".

Gödel found a way to take the statement "This statement is not provable in this formal system" and encode it so as to express it as an equivalent mathematical statement within that formal system. To prove this statement true within the formal system would be to contradict that statement, and therefore it must not be possible to do so, and so the statement must be true.

By a simple step of logic, we humans can see and prove that the statement is true but that it could never be proven to be true within the formal system.

However, a computer program can be thought of as a formal system. In this case, the syntax describes various states in the computer's memory, while the algorithm implemented by the program can be thought of as rules to express how the computer program's state can evolve over time.

It appears that we humans, using our ineffable ingenuity, have done what a formal system such as a computer cannot. It follows, according to Lucas and Penrose, that no computer could ever be truly intelligent, and that we humans are more than mere computing machines.

I don't agree with this interpretation.

Refuting the argument

For a given formal system, we could in principle build a computer program that would prove all the provable statements within that system. Gödel shows that this computer program will never be able to prove all true statements.

However, for any such statements we know to be true, it is possible to invent a more complex formal system which can prove these statements (e.g. by taking the Gödel sentence as an additional axiom). These more complex systems are still incomplete, of course. We can still create further true statements which cannot be proven even by these systems. 

And yet, the point remains that if there is any statement we can prove to be true, but which cannot be proven to be true within a given formal system, there is in fact some more advanced formal system that can prove it to be true. It follows that for any statement we can prove to be true, there exists a computer program which can do likewise.

Now, if the mind is fundamentally computational in nature, then it corresponds to some unimaginably complex formal system. Perhaps the computer program that corresponds to Lucas/Penrose's mind is just complicated enough to prove anything that they can prove and no more. They have no reason to suspect that their minds are capable of proving all true statements, and so they have not shown that human minds are not formal systems.

The mathematician and the formal system

The counter-argument to this view would be that if a mathematician were presented with a book documenting the formal system of her own mind, then she could construct a Gödel sentence for that system. The mathematician would be sure that the sentence is true, however the formal system could not prove it, therefore the mathematician's mind cannot be equivalent to that formal system.

However, there's a big assumption hidden there, and that is that she could understand her own formal system well enough to construct a Gödel sentence for it. Constructing Gödel sentences is not easy, and gets harder the more complex a formal system becomes. There is no reason to believe that any human would be capable of producing a Gödel sentence for their own mind.

In fact, Gödel's incompleteness theorem rather suggests to me that this is impossible, just as no computer program would be capable of generating its own Gödel sentence. To try to achieve either task is akin to trying to fit a rigid container entirely into another of the same size and shape.

Unprovably true

But if mathematicians are formal systems, then there must be true statements of mathematical fact which we could never ever prove. What would this look like, and do we have any examples?

Unfortunately, I cannot give you definite examples of such statements. In fact, this is necessarily impossible. We can never prove the unprovability of a statement which is true, because this leads to a contradiction. Either we can't know for sure that it's true, or we can't know for sure that it's unprovable, simply because we can't know that it's true without being able to prove it!

However, there are many candidates for mathematical statements which we might suspect to be true but unprovable.

One of the simplest to understand is Goldbach's conjecture.

Goldbach's conjecture is that every even number greater than two is expressible as the sum of two prime numbers, e.g. 4 = 2+2, 6=3+3, 8=5+3, etc. No counter-example has ever been found, and so most mathematicians suspect it to be true, and yet nobody has managed to find a proof. This may be because proving it is impossible.

There are many other such examples. Given the abundance of unproven conjectures in mathematics, I am at a loss to explain why Lucas and Penrose assume that Gödel proves that human thought is not computational rather than assuming that, just like all formal systems, we will never be able to prove all true statements.

Consistency

There are a number of other problems with the Lucas/Penrose argument. One of them is that Gödel's theorem only applies to consistent formal systems, that is systems which cannot derive statements which are mutually contradictory.

There is no reason to suppose that human beings are consistent. In fact they rather manifestly seem not to be! People commonly believe all kinds of things that are mutually contradictory. Errors in reasoning are common, and not even the most eminent mathematicians are infallible.

Furthermore, even if a mathematician were perfectly consistent, Gödel's theorem does not apply unless she can prove she is consistent, which is a very tall order.

The Whiteley Sentence

Just to show that you are no more immune to Gödel's trick than a computer, philosopher C.H. Whiteley proposed the following trick.

Suppose I were to say to you: "You cannot prove this sentence".

If you disagree with me, then you believe you can prove the sentence, which says that you cannot prove the sentence. A clear contradiction.

So if you are consistent, then you must agree with me. You must believe something you cannot prove, which in itself is perhaps inconsistent.

However, even though we both agree that you cannot prove the sentence, it seems clear to me that I can prove it by the very same logic I used to show that you could not.

By Lucas and Penrose's logic, it seems that I have shown that my intelligence transcends yours, that my mind is somehow more perfect. Of course this is not so, as you could do precisely the same thing to me. If we are vulnerable to the same trick as formal systems, then why should we suppose that we are not formal systems?

Further Reading
http://www.iep.utm.edu/lp-argue/

Thanks to Fionntan Roukema and Andrew Picken for help with questions about Gödel's theorems.

No comments:

Post a Comment