Faced with such serious problems, David Hilbert (1862-1943), one of the greatest mathematicians of our age, started the study of these formalized theories themselves. He insisted not only on an explicit and unambiguous notation, but also required that it always be possible to check in a finite number of "mechanical" steps whether a sequence of formulae is a proof. Until the 1930's, most mathematicians, Hilbert the most prominent among them, firmly believed that all of mathematics could be developed within these restrictions. In his famous 1900 address entitled Mathematical Problems and in an address On the Infinite in 1925, Hilbert firmly stated this belief. Hilbert and his school spent a lot of effort searching for an effective procedure for checking within a finite number of steps the truth or falsity of mathematical propositions.

However, Hilbert's intuition about the provability of mathematical statements was wrong. In 1931 Kurt Godel proved as a consequence of his famous incompleteness theorem that elementary arithematic is algorithmically undecidable. This means that there does not exist an algorithm for proving the truth or falsity of any proposition of elementary arithmetic.

Since then the existence of many algorithmically undecidable theories and algorithmically unsolvable problems have been proved. An example of such a problem is the so-called 10th problem of a list of 23 problems Hilbert stated in his famous 1900 lecture (some of these problems remain unsolved to this day). The 10th problem is the question whether an arbitrary polynomial equation P(x₁, . . . , x_n) = 0 with integer coefficients has an integer solution. Such an equation is called a Diophantine equation. Matijacevic proved in 1970 that there does not exist an effective procedure deciding whether an arbitrary Diophantine equation has a solution or not.

It is evident that in order to prove negative results like these, it is necessary to know precisely what is meant by computation, a computable function and an algorithm or an effective procedure.

In daily practice a definition is hardly ever necessary, since generally there is little or no difference of opinion whether a proposed procedure may be considered effectively executable or not. This even applies if the procedure is described in imprecise terms.

To achieve general agreement about the non-existence of an effective procedure, however, it is necessary to make this notion mathematically precise

. . .

Problems which can in principle be solved by algorithmic methods but only at insurmountable cost, are not well solved from a practical point of view. The computing community generally agrees to calling a problem solution feasible if the time required for it is at most a polynomial function of the size of the input. Many practical problems of combinatoruial nature, for instance scheduling problems, appear to have no polynomial solution, although it is possible to check in polynomial time whether a proposed answer actually is a solution. The question of whether the class of problems solvable in polynomial time is equal to the class of problems verifiable in polynomial time, the P ?= NP question, is one of the most prominent unsolved problems of complexity theory.