# Understanding of Turing's Answer to the Entscheidungsproblem

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?

• Yes, it's that there are some formulas for which the machine will never find a proof or a disproof so it'll never halt for those inputs. – David Richerby Nov 16 '15 at 8:02

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.