I apologize if this question has been asked before, but I was not able to find a duplicate.I have just finished reading The Annotated Turing and I am a bit confused. From what I understand, the Entscheidungsproblem is whether or not an algorithm exists that can determine whether a statement is provable. In the paper, Turing defines a K machine that will prove all formulae that are provable. This seems almost like a resolution to the problem, but later Turing writes:If the negation of what Gdel has shown had been proved, i.e. if, for  each A, either A or -A is provable, then we should have an  immediate solution of the Entscheidungsproblem. For we can invent a  machine K which will prove consecutively all provable formulae.  Sooner or later K will reach either A or -A. If it reaches A,  then we know that A is provable. If it reaches -A, then, since  K is consistent (Hilbert and Ackermann, p.65), we know that A is not provable.Gdel's Theorem showed that some statements are true, but not provable. I guess what I don't understand is how Gdel's result prevents Turing's K machine from being a solution to the Entscheidungsproblem. Is it just as simple as that there are some formula that the K machine will never encounter, so it will keep running forever and never conclude that the formula is unprovable?
Understanding of Turing's Answer to the Entscheidungsproblem
computability;turing machines;logic;decision problem;incompleteness
What Gdel showed is that there is no finite first-order axiomatization of the theory of the natural numbers. What this means is that if you give a finite list of first-order axioms and schemas, then the corresponding proof system won't be able to prove all true statements about the natural numbers. For example, it won't be able to prove its own consistency (this is Gdel's second incompleteness theorem). (A proof system is consistent if it doesn't prove a statement and its converse.)Turing's machine, when applied to any given finite first-order proof system $\Pi$, will thus be able to prove neither the statement that $\Pi$ is consistent nor its negation.Of course, this is not a proof that the Entscheidungsproblem itself is unsolvable; perhaps there is an altogether different approach that does work. Turing was able to show that, in fact, no (computable) approach works.