Theory of Computation

2.1  A THEORY OF COMPUTABILITY

Computability is the part of logic and theoretical computer science that gives a mathematically precise formulation to the concepts algorithm, mechanical procedure, and calculable function (or relation). Its advent was strongly motivated, in the 1930s, by Hilbert’s program to found mathematics on a (metamathematically provably) consistent (cf. 1.1.1.51) axiomatic basis, in particular by his belief that the Entscheidungsproblem, or decision problem, for axiomatic theories, that is, the problem “is this formula a theorem of that theory?” was solvable by a mechanical procedure that was yet to be discovered.

Now, since antiquity, mathematicians have invented “mechanical procedures”, e.g., Euclid’s algorithm for the “greatest common divisor”,⁴⁹ and had no problem recognizing such procedures when they encountered them. But how do you mathematically prove the nonexistence of such a mechanical procedure for a particular problem? You need a mathematical formulation of what is a “mechanical procedure” in order to do that!

Intensive activity by many [Post (1936, 1944), Kleene (1936), Church (1936b), Turing (1936, 1937), and, later, Markov (1960)] led in the 1930s to several alternative formulations, each purporting to mathematically characterize the concepts algorithm, mechanical procedure, and calculable function. All these formulations were soon proved to be equivalent; that is, the calculable functions admitted by any one of them were the same as those that ...