3
$\begingroup$

The first term is used by Hilbert in his 1928 work, but in Gödel's later work, the same thing is referred to as Unvollständigkeitssatz ("incompleteness theorem"). For today's German CS researchers, it seems Unvollständigkeitssatz is more commonly used, and Entscheidungsproblem ("decision problem") is still understood, but not necessarily associated with das Halteproblem (which seems to be more common after Turing's work on automata). On the other hand, for English CS researchers, Entscheidungsproblem is usually the only word they are familiar with.

Interestingly, when looking at the German Wikipedia, there is no entry for Entscheidungsproblem, but there is one for Gödelscher Unvollständigkeitssatz, and the entry about Hilbert uses Gödelscher Unvollständigkeitssatz. When looking at the English Wikipedia, one readily finds an entry for Entscheidungsproblem.

How come Entscheidungsproblem is no longer used?

$\endgroup$
  • 1
    $\begingroup$ But they are not the same thing. Entscheidungsproblem is a problem that asks for an algorithm deciding whether a given statement is provable from axioms (not necessarily of arithmetic or containing arithmetic), and Unvollständigkeitssatz is a theorem asserting that some statements of arithmetic are neither provable nor disprovable. Even reducing solvability of the first to the second for arithmetic requires accepting the Church–Turing thesis, and even if they were fully equivalent they have clearly distinct meanings. $\endgroup$ – Conifold Mar 1 '17 at 2:53
  • $\begingroup$ Agreed - I have modified my question. But the Unvollständigkeitssätze mean that Entscheidung is in general not going to be possible, right? $\endgroup$ – Frank Mar 1 '17 at 3:10
  • $\begingroup$ Entscheidungsproblem = decision problem: "the problem asks for an algorithm that takes as input a statement of a first-order logic (possibly with a finite number of axioms beyond the usual axioms of first-order logic) and answers "Yes" or "No" according to whether the statement is universally valid". $\endgroup$ – Mauro ALLEGRANZA Mar 1 '17 at 15:07
  • $\begingroup$ Unvollständigkeitssatz reagrsd the incompleteness of sepcific first-order theories, like first-order arithmetic. $\endgroup$ – Mauro ALLEGRANZA Mar 1 '17 at 15:08
4
$\begingroup$

The two problems of completeness (Vollstandigkeit) and decidability of the predicate calculus were clearly defined in 1928 into the first "modern" mathematical logic textbook:

The 1928 edition included a clear statement of the Entscheidungsproblem for FOL, and also asked whether that logic was complete (i.e., whether all semantic truths of FOL [= universally valid (Allgemeingultigkeit) formulas] were theorems derivable from the FOL axioms and rules). The first problem was answered in the negative by Alonzo Church in 1936. The second was answered affirmatively by Kurt Gödel in 1929.

First-order logic is complete but undecidable.

Entscheidungsproblem = decision problem: "the problem asks for an algorithm that takes as input a statement of a first-order logic (possibly with a finite number of axioms beyond the usual axioms of first-order logic) and answers "Yes" or "No" according to whether the statement is universally valid".

The fact that every valid formula can be derived (according to completeness) does not means that we have an algorithm for answering the above question : for first-order logic there is no algorithm like the truth table method for propositional logic.

First-order arithmetic is incomplete [ Unvollständigkeit ].

The two senses of "completeness" are both linked to Gödel, but they are not the same.

The second fundamental result proved by Gödel in 1931 regards the "capability" of the first-order axiomatic theory of arithmetic (FOL calculus plus non-logical axioms) to prove all the true arithmetical sentences.

He found it working on Hilbert's second problem in the attempt to prove consistency of arithmetic.

The underlying calculus is complete but in this case we ask more: the true arithmetical sentences are not universally valid: they are true only in the structures that are models of the axioms.

In a nutshell, Gödel intuited that if a truth predicate $\text {Tr}_F(x)$ could be defined for a certain formal system $F$, then we could derive a version of the liar antinomy.

Hence, such a truth predicate cannot be defined if $F$ is consistent, a result Gödel communicated in letters but never published (it was formally proved by Tarski; see Roman Murawski, Undefinability of Truth. The Problem of Priority: Tarski vs Gödel, History and Philosophy of Logic, Vol.19 (1998)).

Gödel realized that the antinomy can be avoided replacing truth with provability, but this implies that the two notions do not necessarily coincide: $\text{Tr} \ne \text {Pr}$.

But for a sound formal system (i.e. a system that proves only true arithmetical sentences) the only case when truth and provability differ is when $\text{Pr} \subsetneq \text {Tr}$.

In other words, there will be true but formally unprovable sentences.


It is worth noting that not all FOL theories are incomplete and undecidable.

Presburger arithmetic and Skolem arithmetic, the arithmetical theories of "$+$" (plus) and "$\times$" (times) respectively, are both decidable and complete.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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