You may think such problems aren't particularly important, though physicists would disagree, at least concerning the equivalence of manifolds. But another impossibility result is very significant, because it puts a very general limit on what we can ever prove with formal reasoning.

A bit of history first. Many philosophers and mathematicians in the early part of the century were logical positivists, i.e. took the viewpoint that a statement was only meaningful if one could specify a sequence of operations which would decide its truth or falsity. So ``the moon is made of green cheese'' is meaningful, because one can specify spectroscopic tests to determine its consituents, but ``God is good'' isn't, as there are no operations one can perform to examine God. Bertrand Russell was one of the best known positivists.

This stance was closely related to the *formalist* position in
mathematics. This was the view (or hope) that all of mathematics could
be reduced to a set of symbol manipulations. Given any set of axioms,
and a conclusion that you wanted to prove or disprove, all you needed to
do was to manipulate the symbols according to certain formal rules for
constructing proofs. There was no need to appeal to any other notion of
truth. In other words, an operational method should exist for
determining the truth or falsity of mathematical operations.

The German mathematician David Hilbert was a formalist. In the 1920s, he
posed the *decision problem* (also known as the *entscheidungsproblem*, from the German), as part of his programme for
the foundation of mathematics. Is this formalist stance valid? Given a
finite list of logical premises and a conclusion, is there a set of
rules (i.e. an algorithm) that will tell you - for every possible set
of premises and conclusion - whether the conclusion can be proven from
the premises?

In 1931, Gödel answered part of this. Given any logical system
that's powerful enough to describe arithmetic, it's impossible to show,
by using the system's own rules of inference, that it is both consistent
and complete. *Consistent* means that the system can't prove
something to be both true and false. *Complete* means that it's
possible to prove *every* statement either true or false. What
Gödel showed was that in any logical system that's powerful enough
to describe arithmetic, there is a statement that you can show to be
true by reasoning outside the system, but that the system's own rules of
inference can't prove.

Hilbert's programme also called for solution to whether any axiomatic
system can be *decideable* - i.e. whether there exists a definite
method which in principle can be applied to determine the truth of any
assertion. Gödel had answered part of this for arithmetic, but the
general problem - whether for any logical system, you could prove
every statement - was still unresolved. Turing was attracted by this,
and decided to work on it. In 1936, he showed the answer that there
wasn't. In doing so, he also defined and answered the *halting
problem*. So I need now to describe the halting problem, and to talk
about Turing's notion of ``definite method'' or computation.

Incidentally, I am typing this in a great hurry, and even if it's
intelligible, it may not be completely accurate. There are various
references. A book which should shortly appear in the library is *Searching for Certainty* by John Casti. Chapter Six is a popular account
of Turing machines, Gödel's theorem, the limitations on theories,
and so on. AI photocopy D77, *What is a Computation?* by Martin Davis (from *Mathematics Today* edited by L.A.Steen, Springer-Verlag 1978), gives a
slightly more technical account, including the proof of the halting
problem for Turing machines, and an unsolveable word problem.

Wed Feb 14 23:47:23 GMT 1996