What is the definition of the Entscheidungsproblem (Decision Problem)?

Question

I have been trying to find the most “formal” definition of the Entscheidungsproblem for the past couple of days now.

On Wikipedia it states this:

The problem asks for an algorithm that considers, as input, a statement and answers "Yes" or "No" according to whether the statement is universally valid, i.e., valid in every structure satisfying the axioms.

On Simple English Wikipedia, it states this:

Is there an algorithm that will take a formal language, and a logical statement in that language, and that will output "True" or "False", depending on the truth value of the statement?

In these instances, are the two definitions equivalent? Is taking the formal language equivalent to considering whether the statement is universally valid?

Another definition, this one found on Quora, states this:

Is there an effective procedure (an algorithm) which, given a set of axioms and a mathematical proposition, decides whether it is or is not provable from the axioms?

Out of these definitions, which one is the most formal definition of the Entscheidungsproblem? Why does that definition adhere to the Entscheidungsproblem more closely than the other ones?

Just to add, I also tried to find the definition or an outline of the problem from the Principle of Mathematical Logic book – but I could not get through the dense layer of prerequisite knowledge. Perhaps there’s a section in the book that describes it in layman’s term. If there is, I would greatly appreciate it if someone could tell me where I can find that section.

Sorry if this sort of question is a little vague.

Answer 1

None of those definitions is entirely accurate, since the following terms are left undefined:

• "The axioms:" what axioms exactly? (Note that the other terms, e.g. "structure," are actually unambiguous technical terms - and on that note see the end of this answer.)

• "True"/"False:" according to what notion of truth? (Unsurprisingly given that this is the Simple English Wikipedia article, this is the most dangerous conflation.)

• "Set of axioms:" what sort of set of axioms is allowed here, and how should a set of axioms be "given?"

Here is a precise definition of the Entscheidungsproblem. We start small. Suppose $T$ is a finite first-order theory $T$ in a finite language.$^*$ Then there is an "Entscheidungsproblem for $T$,"$^\dagger$ which I'll call $E(T)$:

Is there an algorithm for determining whether a sentence $\sigma$ in the language of $T$ is provable from $T$?

Note that for some $T$s the answer to $E(T)$ is yes, e.g. Presburger arithmetic.

The full Entscheidungsproblem can then be phrased as follows (and my understanding is that this is the most faithful to its original intent):

Is the answer to $E(T)$ always yes?

It turns out that we can boil this down to a single candidate: there is such a theory $T$ (actually, there are many such theories) such that $E(T)$ is maximaly complicated. For example, we can take Robinson arithmetic $\mathsf{Q}$. (Note that strictly speaking, according to the phrasing above something like first-order Peano arithmetic or $\mathsf{ZFC}$ does not count, being non-finitely-axiomatizable.) So we could equivalently phrase the Entscheidungsproblem as:

Is there an algorithm for determining whether a sentence $\sigma$ in the language of arithmetic is provable from $\mathsf{Q}$?

There are yet more rephrasings of the Entscheidungsproblem, the most nontrivial one being in terms of structures:

Is there an algorithm for determining whether a sentence $\sigma$ in the language of arithmetic is true in every model of $\mathsf{Q}$?

The equivalence between these notions is highly nontrivial - it's a consequence of Godel's completeness theorem (that's not a typo!).

And of course the modern perspective on the Entscheidungsproblem is that it's really just a rephrasing of the halting problem, so we tend to talk about that instead. One direction of this conflation is that the above $E(T)$s can be directly encoded in the halting problem, and the other direction is that we show the undecidability of $E(\mathsf{Q})$ by coding the halting problem into it - $E(\mathsf{Q})$ and the halting problem are equivalent in a precise sense.

---

$^*$Why finite language? Well, I want to avoid issues with the complexity of the language itself - the focus should be just on what the theory can do, not how hard it is to describe the theory or understand the language in the first place. It's really more natural to allow arbitrary computable theories in computable languages, but I think restricting attention to the finite case makes things simpler at first.

$^\dagger$See e.g. Church page $363$: "As a corollary of Theorem XIX, it follows that the Entscheidungs-problem is unsolvable in the case of any system of symbolic logic which is $\omega$-consistent [...] and is strong enough to allow certain comparatively simple methods of definition and proof. "