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 Gödel 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.
Gödel's Theorem showed that some statements are true, but not provable. I guess what I don't understand is how Gödel'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?