Godel's Incompleteness Theorem
Gödel's incompleteness theoremsare two theorems of mathematical logic that demonstrate the inherent limitations of every formal axiomatic system containing basic arithmetic. These results, published by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of mathematics. The theorems are widely, but not universally, interpreted as showing that Hilbert's program to find a complete and consistent set of axioms for all mathematics is impossible.
The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an effective procedure(i.e., an algorithm) is capable of proving all truths about the arithmetic of the natural numbers. For any such formal system, there will always be statements about the natural numbers that are true, but that are unprovable within the system. The second incompleteness theorem, an extension of the first, shows that the system cannot demonstrate its own consistency.
Employing a diagonal argument, Gödel's incompleteness theorems were the first of several closely related theorems on the limitations of formal systems. They were followed by Tarski's undefinability theorem on the formal undefinability of truth, Church's proof that Hilbert's Entscheidungsproblem is unsolvable, and Turing's theorem that there is no algorithm to solve the halting problem.
Entscheidungs problem
The Entscheidungs problem is a challenge posed by David Hilbert and Wilhelm Ackermann in 1928.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 isuniversally valid, i.e., valid in every structure satisfying the axioms. By the completeness theorem of first-order logic, a statement is universally valid if and only if it can be deduced from the axioms, so the Entscheidungsproblem can also be viewed as asking for an algorithm to decide whether a given statement is provable from the axioms using the rules of logic.
In 1936, Alonzo Church and Alan Turing published independent papersshowing that a general solution to theEntscheidungsproblemis 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.
https://en.wikipedia.org/wiki/Entscheidungsproblem
References
https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems