be used for a similar proof of undecidability) ... Thus, we have a proposition before us which asserts its own unprovability [15]. (His footnote 15: Contrary to appearances, such a proposition is not circular, for, to begin with, it asserts the unprovability of a quite definite formula)". Halting problem: Turing's first proof The Entscheidungsproblem, the decision problem, was first answered by Church in April 1935 and preceded Turing by over a year, as Turing's paper was received for publication in May 1936. Turing's proof is made difficult by number of definitions required and its subtle nature. See Turing machine and Turing's proof for details. Turing's first proof (of three) follows the schema of Richard's paradox: Turing's computing machine is an algorithm represented by a string of seven letters in a "computing machine". Its "computation" is to test all computing machines (including itself) for "circles", and form a diagonal number from the computations of the non-circular or "successful" computing machines. It does this, starting in sequence from 1, by converting the numbers (base 8) into strings of seven letters to test. When it arrives at its own number, it creates its own letter-string. It decides it is the letter-string of a successful machine, but when it tries to do this machine's (its own) computation it locks in a circle and can't continue. Thus, we have arrived at Richard's paradox. (If you are bewildered see Turing's proof for more). A number of similar undecidability proofs appeared soon before and after Turing's proof: April 1935: Proof of Alonzo Church ("An Unsolvable Problem of Elementary Number Theory"). His proof was to "...propose a definition of effective calculability ... and to show, by means of an example, that not every problem of this class is solvable" (Undecidable p. 90)) 1946: Post correspondence problem (cf Hopcroft and Ullman p. 193ff, p. 407 for the reference) April 1947: Proof of Emil Post (Recursive Unsolvability of a Problem of Thue) (Undecidable p. 293). This has since become known as "The Word problem of Thue" or "Thue's Word Problem" (Axel Thue proposed this problem in a paper of 1914 (cf References to Post's paper in Undecidable, p. 303)). Rice's theorem: a generalized formulation of Turing's second theorem (cf Hopcroft and Ullman p. 185ff) Greibach's theorem: undecidability in language theory (cf Hopcroft and Ullman p. 205ff and reference on p. 401 ibid: Greibach [1963] "The undecidability of the ambiguity problem