The Entscheidungsproblem (decision problem)



What is the Entscheidungsproblem and why did Alan Turing & Alonzo church determine it to be impossible?

Most broad description I’ve got is “a challenge to create an algorithm that accepted formal language input, a logical statement in that language, and answered whether or not the statement expression was universally true or false for the language,” which I still don’t understand.


In: Mathematics

So the question is, “I wrote a program and you wrote a program, do they do exactly the same thing?” In the discussion you may read they use term “lamda calculus (function).” This means in English, a program.

A computer can’t determine that in most cases. Which is sort of surprising.

EDIT: why can’t you? Because you can’t anticipate an infinite variety of inputs. So you can do a truth table which has limited number of inputs. Just not all programs.

A related concept is a computer can’t determine if a program will run to completion without errors. A computer can’t calculate that by shortcut, you have to run the program and find out.

Basically, you start with a set of axioms. For example:

* You have at most 10 cakes.
* You have 5 chocolate cakes.

There are different models that satisfy those axioms – for example, you can have only 5 chocolate cakes, or you can have 5 chocolate cakes and 3 cheesecakes.

Then, you want to judge whether a statement is universally true or false from the set of axioms. Equivalently, it has to be true in all structures that satisfies them.

* Is it true that there are at least 4 chocolate cakes? **Yes**.
* Is it true that there are 6 non-chocolate cakes? **No (is never true)**.
* Is it true that there is some non-chocolate cake? **No (not always true)**.

When you formulate a correct sentence in the language of cakes, there is always an answer of **Yes** (if all structures satisfy that) or **No** (axioms don’t imply it).

Even though there is always an answer (which you generally don’t know), it’s important to figure out whether there is a consistent algorithm / computation (no matter how difficult) that tells you the answer.

Edit: In the language of cakes, decision problem is actually solved (it’s got finitely many non-isomorphic models). The important thing is:

However, Gödel’s result is, that **most often, it’s not that simple** – there is often no such computation that determines whether the answer is yes or no – in particular, if there is some arithmetic (embedding of natural numbers) in the language.

A famous example is Halting problem (“does the computer program run infinitely?”). This is a valid question in the language of computational logic, however, there is no consistent algorithm that determines it. You can generally determine it for a single program, but there is no automatization that would handle this consistently for all of them.