Let’s suppose that there is a machine M that can do the job we envisaged for a consistent system.

That is, the machine can prove or disprove any theorem that we feed to it. It is programmed with the axioms of the system and it can use them to provide proofs.

Now suppose we ask for the program for the machine written in the same logic used for the theorems that the machine proves. After all any computer can be reduced to logic and all we are requesting is the logical expression that represents the design of the computer – call this PM for "Program for M".

Now we take PM and construct a logical expression which says

“The machine constructed according to PM will never prove this statement is true”

and call this statement X.

Now we ask the machine to prove or disprove X.

Consider the results. If the machine says “yes this is true” then the statement is false. If the machine says that the statement is false then the statement is true.

The proof that there are theorems that cannot be proved

You see what the problem is here and you can do this sort of trick with any proof machine that is sufficiently powerful to accept its own description as a theorem.

Any such machine, and the system of logic on which it is based, must, by its very nature be inconsistent in that there are theorems that can be written using the system that it cannot be used to prove either true or false.

In other words there are three types of theorem in the system – those that are provably true, those that are provably false and those that are undecidable using the axioms that we have at our disposal.

OK, you may say but is it possible to for a machine to be powerful enough to attempt to prove a statement that involves its own description? Perhaps it is in the nature of machines that they cannot cope with their own description.

The really clever part of Gödel’s work was to find that any axiomatic system powerful enough to describe the integers, i.e. powerful enough to describe simple arithmetic, has this property.

That is arithmetic isn’t a consistent axiomatic theory which means that there are theorems about the integers that have no proof or disproof within the theory of arithmetic.

So now think about the 300-year search for a proof for Fermat’s last theorem.

Perhaps it wasn’t that the mathematicians weren’t trying hard enough. Perhaps there was no proof. As it turns out we now know that a proof exists but there was a long time when it was a real possibility that the theorem was undecidable.

You clearly understand the idea but do you believe it?

Consider the following problem: there seem to be lots of paired primes i.e. primes that differ by two (3,5), (5,7), (11,13) and so on. It is believed that there are an infinite number of such pairs - the so called "twin prime conjecture" but so far no proof.

So what are the possibilities?

You examine number pairs moving over larger and large integers and occasionally you meet paired primes.

Presumably either you keep on meeting them or you there comes a point when you don’t.

In other words, the theorem is either true or false. And as it is true or false presumably there should be a proof of this.

If you have taken Gödel’s theorem to heart you should know that this doesn’t have to be the case. The integers go on forever and you can’t actually decide the truth of the theorem by looking at the integers.

How far do you have to go without seeing a pair of primes to be sure that you aren’t ever going to see another pair?

How many pairs do you have to see to know that you are going to keep seeing them?

There is no answer to either question. In the same way why do you assume that there is a finite number of steps in a proof that will determine the answer.

Why should the infinite be reducible to the finite?

Only because we have grown accustomed to mathematics performing this miracle.

In the case of the twin prime conjecture recent progress has proved that that are infinitely many primes separated by N and N has to be less than 70 million. This doesn't mean that N is 2 however. Collaborative work by a lot of mathematicians has reduced the upper limit (at the end of 2013) to less than 576 which seems like progress. Can the bound be pushed down as far as 2 or is there really no proof?

Fermat’s last theorem stated that the only integer solution to a particular equation was when n equals 2. To prove this the hard way requires examining the equation for n equal to 1, 2, 3… and for all a,b and c and this means we have to test an infinite number of possibilities.

Yet we have a finite proof.

We have a logical derivation of the truth of the theorem, which doesn’t involve testing an infinite number of cases.

This is what Gödel’s theorem really is all about.

There are statements that are undecidable. If you add additional axioms to the system the statements that were undecidable might well become decidable but there will still be valid statements that are undecidable. Indeed every time you expand the axioms you increase the number of theorems that are decidable and undecidable.

It’s as if mathematics at the turn of the 20th century was seeking the ultimate theory of everything and Gödel proved that this just wasn’t possible.

So far so good, or bad depending on your point of view.

You may even recognise some of this theory as very similar to the theory of Turing machines and non-computability, in which case it might not be too much of a shock to you. However, at the time they were thought up both Gödel’s and Turing’s ideas were revolutionary and they were both regarded with suspicion and dismay.

It was thought to be the end of the dream: mathematics was limited. Mathematics wasn’t perfect and in fact every area of mathematics contained its limitations.

Today you will find it argued that Gödel’s theorem proves that god exists. You will find it argued that Gödel’s theorem proves that human thought goes beyond logic. The human mind is capable of seeing truth that mathematics cannot prove. It is also argued that it limits artificial intelligence, because there are things that any machine cannot know and hence also proves that human intelligence is special because it can know what the machine cannot.

If you think about it, Gödel’s theorem proves none of this. It doesn’t even suggest that any of this is the case.

Gödel’s theorem doesn’t deal with probabilities and what we believe, only in the limitations of finite systems in proving assertions about the infinite.

Sometimes the infinite is regular enough to allow something to be proved. Sometimes, in fact most of the time, it isn’t.

But important though this is we live in a finite personal universe and we don’t demand perfect proof. We go with the flow, guess and accept good probabilities as near certainties.

The sort of instructions that most computers recognize are too simple for humans to be bothered with - and so we invented assembly language. Find out how it works and how it started the whole movement [ ... ]

Computational grammar is a subject that is sometimes viewed as a form of torture by computer science students, but understanding something about it really does help ....