‘A Note of the Entscheidungsproblem,’ pp. 40-41 in The Journal of Symbolic Logic, Vol. 1, No. 1, March 1936.
New York: The Association for Symbolic Logic, Inc., 1936. First edition, journal issue in the original printed wrappers, of Church’s solution to the ‘Entschedungsproblem’ (‘decision problem’). “Church’s paper, submitted on April 15, 1936, was the first to contain a demonstration that David Hilbert’s Entscheidungsproblem – i.e., the question as to whether there exists in mathematics a definite method of guaranteeing the truth or falsity of any mathematical statement – was unsolvable. Church did so by devising the ‘lambda-calculus.’ A few months earlier, Church had earlier shown the existence of an unsolvable problem of elementary number theory [although this was published later than the present paper], but [the offered] paper was the first to put his findings into the exact form of an answer to Hilbert’s ‘Entscheidungsproblem.’ Church’s paper bears on the question of what is computable, a problem addressed more directly by Alan Turing in his paper ‘On computable numbers,’ published a few months later (OOC). Turing’s proof was via his ‘Turing machines.’ “Church got it right and he got it first. By any purely quantifiable evaluation Church’s contribution was at least as important as Turing’s (Robert Irving Soare in Alan Turing, his work and impact, p. 67). Both the lambda-calculus and Turing machines have proved to be of seminal importance, not only for mathematical logic, but also for the development of computer science. “The decision problem was brought to the fore of mathematics by the German mathematician David Hilbert (who in a lecture given in Paris in 1900 set the agenda for much of twentieth-century mathematics). In 1928 Hilbert described the decision problem as ‘the main problem of mathematical logic’, saying that ‘the discovery of a general decision procedure is a very difficult problem which is as yet unsolved’, and that the ‘solution of the decision problem is of fundamental importance’… Hilbert’s requirement that the system expressing the whole content of mathematics be decidable amounts to this: there must be a systematic method for telling, of each mathematical statement, whether or not the statement is provable in the system… The project of expressing mathematics in the form of a complete, consistent, decidable formal system became known as ‘proof theory’ and as the ‘Hilbert programme’… “Unfortunately for the Hilbert programme, however, it was soon to become clear that most interesting mathematical systems are, if consistent, incomplete and undecidable … In his incompleteness theorem, [Kurt] Gödel had shown that no matter how hard mathematicians might try to construct the all-encompassing formal system envisaged by Hilbert, the product of their labours would, if consistent, inevitably be incomplete … Gödel’s theorem left the question of decidability open” (Copeland, The Essential Turing, pp. 46-8). Any attempt to solve the Entscheidungsproblem hinges on exactly what is meant by saying that a function can be calculated by a finite algorithm, or that it is ‘effectively calculable.’ Turing later summarized the possibilities in his thesis (‘Systems of logic based on ordinals,’ 1939): “A function is said to be ‘effectively calculable’ if its values can be found by some purely mechanical process. Although it is fairly easy to get an intuitive grasp of this idea, it is nevertheless desirable to have some more definite, mathematically expressible definition. Such a definition was first given by Gödel at Princeton in 1934 ... These functions are described as ‘general recursive’ by Gödel ... Another definition of effective calculability has been given by Church [in the present paper] ... who identifies it with lambda-definability. The author has recently suggested [in ‘On computable numbers’] a definition corresponding more closely to the intuitive idea. It was stated above that “a function is effectively calculable if its values can be found by some purely mechanical process”. We may take this statement literally, understanding by a purely mechanical process one which could be carried out by a machine. It is possible to give a mathematical description, in a certain normal form, of the structures of these machines. The development of these ideas leads to the author’s definition of a computable function, and to an identification of computability with effective calculability.” Church’s student Stephen Kleene had proved in 1935 that the notions of ‘general recursive’ and ‘lambda-definable’ are equivalent, and Church proposed in the present paper that these should be taken as the definition of ‘effective calculability.’ Church “had developed a formalism called the 'lambda-calculus' and, with the logician Stephen Kleene, had discovered that this formalism could be used to translate all the formulae of arithmetic into a standard form. In this form, proving theorems was a matter of converting one string of symbols of the lambda-calculus into another string, according to certain rather simple rules. Church had then been able to show that the problem of deciding whether one string could be converted into another string was unsolvable, in the sense that there existed no formula of the lambda-calculus which could do it. Having found one such unsolvable problem, it had become possible to show that the exact question that Hilbert had posed must also be unsolvable. But it was not obvious that ‘a formula of the lambda-calculus’ corresponded to the notion of a ‘definite method’. Church gave verbal arguments for the assertion that any 'effective' method of calculation could be represented by a formula of the lambda-calculus” (Hodges, Alan Turing: The Enigma, p. 112). Knowing nothing about Church’s work, Turing had been working on the decision problem, having been inspired by lectures of Max Newman. Just days after Turing completed his own solution, Newman received a copy of Church’s paper. “It pre-empted the result, and threw into jeopardy the publication of Alan’s work, scientific papers not being allowed to repeat or copy one another” (Hodges, p. 112). Turing’s approach was very different from Church’s, however, and Turing’s paper was submitted on 28 May 1936 to the London Mathematical Society for publication in its Proceedings. The following day Turing wrote to his mother: Meanwhile a paper has appeared in America, written by Alonzo Church, doing the same things in a different way. Mr Newman and I have decided however that the method is sufficiently different to warrant the publication of my paper too. Alonzo Church lives at Princeton so I have decided quite definitely about going there. “Newman wrote on 31 May to the Secretary of the London Mathematical Society, F.P. White, explaining the position: I think you know the history of Turing's paper on Computable numbers. Just as it was reaching its final state an offprint arrived, from Alonzo Church of Princeton, of a paper anticipating Turing's results to a large extent. I hope it will nevertheless be possible to publish the paper. The methods are to a large extent different, and the result is so important that different treatments of it should be of interest. The main result of both Turing and Church is that the Entscheidungsproblem on which Hilbert's disciples have been working for a good many years — i.e. the problem of finding a mechanical way of deciding whether a given row of symbols is the enunciation of a theorem provable from the Hilbert axioms — is insoluble in its general form. “Turing’s paper was revised in August to include a note (p. 231) referring to Church’s: “In a recent paper Alonzo Church has introduced an idea of ‘effective calculability’, which is equivalent to my ‘computability’, but is very differently defined. Church also reaches similar conclusions about the Entscheidungsproblem. The proof of equivalence between ‘computability’ and ‘effective calculability’ is outlined in an appendix to the present paper.” Turing’s paper appeared in two parts, in the issues dated 30 November and 23 December 1936. “Alan Turing began working on the Entscheidungsproblem with no knowledge of what Church was doing. He began with his own explication of algorithmic solvability, or as he called it, computability, in terms of extremely simple abstract computing machines, what are now called ‘Turing machines’. By analyzing what someone actually does when computing something, he provided a convincing argument for the adequacy of his formulation. (Later he proved that his concept was equivalent to Church’s.) Like Church, he used what he had done to prove that a certain specific problem is unsolvable. In Turing’s case the unsolvable problem was to determine algorithmically whether one of his given machines would ever produce a particular symbol, the so-called ‘printing problem’” (Davis in in Alan Turing, his work and impact, p. 51). One formulation of the Entscheidungsproblem is: “Find an algorithm to determine whether a given sentence of first order logic is valid, that is, true regardless of what specific objects and relationships are being reasoned about … By using sentences of first order logic to mimic the step-by-step behaviour of his machines he was able to associate with any one of his machines a corresponding sentence of first order logic that is valid if and only if that machine eventually produces the symbol 0. Thus an algorithm for validity would automatically provide a solution to the printing problem, although it is, in fact, unsolvable. Thus Turing could conclude that the Entscheidungsproblem is algorithmically unsolvable” (ibid., pp. 49-51). “Poor news though the unsolvability of the Entscheidungsproblem was for the Hilbert school, it was very welcome news in other quarters, for a reason that Hilbert's illustrious pupil von Neumann had given in 1927: ‘If undecidability were to fail then mathematics, in today's sense, would cease to exist; its place would be taken by a completely mechanical rule, with the aid of which any man would be able to decide, of any given statement, whether the statement can be proven or not.’ As the Cambridge mathematician G. H. Hardy said in a lecture in 1928: ‘if there were ... a mechanical set of rules for the solution of all mathematical problems ... our activities as mathematicians would come to an end’” (Copeland, p. 53). OOC 250.
8vo (255 x 178 mm), pp. 44. Original printed wrappers, a very fine copy.
Item #5483
Price: $2,800.00
