have to execute an algorithm. Thus the algorithm was implicitly part of the logical apparatus used to generate mathematics. It was clear to Turing and Church that a formal understanding of the nature of these algorithms was necessary. To that end Turing formulated what is now known as the Turing machine (at the time, of course — 1937 — it was purely conceptual), and at about the same time Church developed an equivalent approach, the lambda calculus. An algorithm was considered legitimate as a procedure if it could be described as a Turing machine or formulated in the lambda calculus. Each algorithm corresponded to a particular Turing machine. A Turing machine was required to have a finite number of states, and a proof calculated on the machine would need to finish in a finite number of steps. By proving that it could not in general be shown whether or not algorithms would execute in a finite number of steps (the halting problem), Turing demonstrated, in results analogous to G[ö]{}del’s, that some propositions were not provable. Church arrived at the same result using his lambda calculus. The results of G[ö]{}del, Turing, and Church showing that it is impossible to prove that 