7
$\begingroup$

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?

Improve this question
$\endgroup$
1
  • 2
    $\begingroup$ 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. $\endgroup$
    – David Richerby
    Commented Nov 16, 2015 at 8:02

2 Answers 2

Reset to default
5
$\begingroup$

What Gödel 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 Gödel'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.

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ "Finite first-order axiomatization of the theory of natural numbers" should be "computably enumerable axiomatization of the true theory of natural numbers". A scheme does not count as "one axiom". $\endgroup$
    – Andrej Bauer
    Commented Nov 16, 2015 at 9:25
0
$\begingroup$

It is not correct. Robinson arithmetic system is finite axioms system, which is incomplete same as Peano axioms system.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.