Entscheidungsproblem

https://en.wikipedia.org/wiki/Entscheidungsproblem

The Entscheidungsproblem, aka the decision problem, is a challenge posed by David Hilbert and Wilhelm Ackermann in 1928. The problem in question is whether an algorithm, described as follows, could possibly exist: The algorithm is given an input statement, which it is expected to process, then reply affirmatively or negatively as to whether the input statement is universally valid (valid in every structure that satisfies a particular set of axioms).

By the completeness theorem of first-order logic, a statement is universally valid iff it can be deduced from the axioms, so the Entscheidungsproblem can also be viewed as asking for the existence of an algorithm that can decide whether a given statement is provable from the axioms using the rules of logic.

In 1936, Alonzo Church and Alan Turing published independent papers showing that a general solution to the Entscheidungsproblem is impossible, assuming that the intuitive notion of "effectively calculable" is captured by the functions computable by a Turing machine (or equivalently, by those expressible in the lambda calculus). This assumption is now known as the Church-Turing thesis.