The decision problem

Next: Turing-equivalent computersand Turing-computable problems
Up: No Title
Previous: Complete impossibilities
Back: to main list of student notes

# The decision problem

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.

Next: Turing-equivalent computersand Turing-computable problems
Up: No Title
Previous: Complete impossibilities
Back: to main list of student notes

Jocelyn Ireson-Paine
Wed Feb 14 23:47:23 GMT 1996