The Decision Problem

The Decision Problem

One of the most influential formulations of what would come to be known as the Decision Problem—Entscheidungsproblem in the original German—appears in the work published in 1928 by David Hilbert and Wilhelm Ackermann, Grundzüge der theoretischen Logik, or Principles of Theoretical Logic, which brought together some of the most important logical discoveries accumulated up to the beginning of the twentieth century.

The term had already appeared in Heinrich Behmann’s work during the early 1920s, but it was Hilbert and Ackermann’s formulation that turned the problem into one of the central objectives of Mathematical Logic.

The problem can be summarized as follows:

Given a formula of First-Order Logic, we ask whether there exists an effective method capable of deciding in a finite number of steps whether or not that formula is logically valid. The procedure must always terminate and return an answer: “yes” or “no.”

The problem can also be formulated syntactically: determining whether a formula is provable by means of the axioms and rules of a logical calculus. Gödel’s Completeness Theorem would later establish that, for First-Order Logic, a formula is valid if and only if it is provable. Therefore, in a complete calculus, the semantic and syntactic formulations of the problem coincide.

Note that a decision procedure need not provide a proof when it returns an affirmative answer. What is essential is the existence of an algorithm that, for any formula, terminates and correctly determines which of the two answers applies.

Hilbert and Ackermann presented the Decision Problem as one of the principal problems of Mathematical Logic as a whole.

Decidability in Propositional Logic

Let us focus for a moment not so much on the syntactic aspect—whether or not a formula is provable from the axioms—as on the semantic one, that is, whether a formula can be true under some interpretation. This leads us to the concept of satisfiability: a formula is satisfiable if there is at least one interpretation under which it is true.

In the series devoted to Mathematical Logic, we explained that formulas of Propositional Logic can be contradictions, always false—such as \(P\land\neg P\)—or tautologies, always true—such as \(P\lor\neg P\). Between these two extremes lie contingent formulas, true under some interpretations and false under others.

Both tautologies and contingent formulas that are true under at least one interpretation are satisfiable. Only contradictions are unsatisfiable.

Propositional Logic is decidable: it is possible to answer, by means of a finite procedure, whether a formula is satisfiable, valid, or contradictory. One of the most elementary methods for doing so is the Truth Table.

Each of the variables \(A\), \(B\), and \(C\) in the formula can take one of two truth values: true, represented by \(1\), or false, represented by \(0\). The truth value of the complete formula can be checked by evaluating the table for every possible combination of values assigned to the variables.

If the formula is true in at least one row, it is satisfiable. If it is true in every row, it is a tautology; if it is false in every row, it is a contradiction. If, as in the example, only one interpretation makes it false, the formula is satisfiable and contingent, but it is not a tautology.

Decidability and the Decision Problem

We may then ask the following question: is First-Order Logic decidable in the same way as Propositional Logic? Can we find a method that determines, for any formula, whether it is valid or satisfiable?

These two questions are closely related. A formula \(A\) is valid when it is true under every possible interpretation. Therefore, \(A\) is valid if and only if its negation \(\neg A\) is not satisfiable. A procedure that decided satisfiability would also make it possible to decide validity, and vice versa.

In Predicate Logic, or First-Order Logic, semantic interpretation is more complex than in Propositional Logic. We must select a domain of objects and assign to each predicate symbol a property or relation defined over that domain.

For example, if we interpret a formula \(P(x)\) as “\(x\) is a prime number” and take the natural numbers as the domain of reference, the predicate \(P\) is interpreted as the set of all prime numbers. Each instance then receives a truth value:

$$P^{T}(1)=0$$

$$P^{T}(2)=1$$

$$P^{T}(3)=1$$

$$P^{T}(4)=0$$

$$P^{T}(5)=1$$

$$\vdots$$

The open formula \(P(x)\) does not by itself have a single truth value: this depends on the value assigned to \(x\). A closed formula such as \(\exists x\,P(x)\), however, does express a proposition that is true or false within a complete interpretation.

Satisfiability and Cardinality

It is not always necessary to examine interpretations one by one in order to confirm that a formula is satisfiable. There are formulas such as \(\Psi(x)\lor\neg\Psi(x)\) that are true for every interpretation of the predicate \(\Psi\), every domain, and every value assigned to \(x\).

But consider a formula such as the following:

$$\exists x\exists y\left[\Psi(x)\land\neg\Psi(y)\right]$$

Is there any case in which this formula is true? The answer depends on the interpretation. In a domain containing a single object, \(x\) and \(y\) would necessarily designate the same individual. The formula would then reduce to an expression of the form \(\Psi(x)\land\neg\Psi(x)\), which is contradictory.

In a domain containing two or more objects, however, the formula is satisfiable: it is enough to interpret \(\Psi\) so that one object satisfies the predicate and another does not. The formula is not true under every interpretation of such domains, but there is at least one interpretation that makes it true.

Other formulas impose different conditions on the number of objects in the domain. For example:

$$\forall x\forall y\left[x=y\right]$$

can only be true in a domain containing a single individual. By contrast:

$$\exists x\exists y\left[x\neq y\right]$$

requires the domain to contain at least two objects.

Hilbert and Ackermann thus emphasized the close relationship between the satisfiability of a formula and the cardinality of the domain under which it is interpreted. A formula may have models of certain cardinalities and lack them at others.

If a formula has a model whose domain has a certain cardinality, we can transport the interpretation to any other domain of the same cardinality by means of a one-to-one correspondence. But this does not mean that satisfiability is determined solely by a number: we must also specify how the predicates, relations, and functions of the language are interpreted.

Truth Tables

Now consider a formula such as \(\exists x\left[Q(x)\right]\), interpreted over a three-element domain: \(\{\alpha,\beta,\gamma\}\). To determine its truth value, we must consider the three instances \(Q(\alpha)\), \(Q(\beta)\), and \(Q(\gamma)\). We can transform the original formula into an equivalent disjunction of Propositional Logic:

$$Q_{\alpha}\lor Q_{\beta}\lor Q_{\gamma}$$

In the case of \(\forall x\left[Q(x)\right]\), its propositional equivalent would be a conjunction:

$$Q_{\alpha}\land Q_{\beta}\land Q_{\gamma}$$

This operation is feasible for formulas with more variables and for domains containing any finite number of elements. If predicates with several variables appear, we must consider every possible combination of elements in the domain.

Once this finite expansion has been carried out, we can apply a Truth Table. It is therefore possible to decide whether a formula has a model of a previously fixed finite cardinality.

This resolves certain particular cases, but not yet the general Decision Problem. To solve it, we would need a procedure capable of determining satisfiability without knowing in advance the size of a possible model.

Infinity in the Decision Problem

We could successively examine domains of one, two, three, and more elements, applying the preceding procedure in each case. If the formula has some finite model, we would eventually find it.

However, this procedure does not always terminate. If the formula is not satisfiable, we could continue indefinitely increasing the size of the domain without ever reaching a negative answer. It would likewise fail to terminate if the formula had only infinite models.

Moreover, it is not true that every formula satisfiable in a finite domain is satisfiable in all larger domains. The formula \(\forall x\forall y\left[x=y\right]\), for example, has a one-element model, but none with two or more elements.

There are also formulas that can only be satisfied in infinite domains. Here is an example:

$$\left(\forall x\exists y\,F(x,y)\right)\land\left(\forall x\,\neg F(x,x)\right)\land\left(\forall x\forall y\forall z\left[(F(x,y)\land F(y,z))\rightarrow F(x,z)\right]\right)$$

This formula is satisfied, for example, if we interpret \(F(x,y)\) as “\(x\) is less than \(y\)” over the domain of the natural numbers. The first part states that every object is related to another; the second establishes that no object is related to itself; and the third imposes transitivity on the relation.

The formula cannot be satisfied in any finite domain. If there were only finitely many objects and each had a successor according to \(F\), we would eventually repeat one of them. Transitivity would then produce a cycle and, ultimately, a relation of the form \(F(x,x)\), which is prohibited by the second condition.

Therefore, Truth Tables generalized to finite domains are not sufficient to decide First-Order Logic. The existence of exclusively infinite models does not by itself prove that the Decision Problem is unsolvable, but it does show why the method used for Propositional Logic cannot be extended directly to the general case.

Conclusion

In 1928, the Decision Problem remained unsolved. Methods capable of deciding particular fragments of First-Order Logic were known, but it was not known whether there was a general procedure that worked for every formula. Behmann, Bernays, Schönfinkel, Ackermann, and other authors obtained positive results for certain classes of expressions without reaching a complete solution.

The definitive answer would be negative. In 1936, Alonzo Church proved that there is no general algorithm for determining the provability of every formula of First-Order Logic. That same year, Alan Turing independently reached an equivalent result through his analysis of computing machines.

Gödel’s incompleteness theorems, which we will study in the following articles, must not be confused with this unsolvability result. The Decision Problem asks whether there is a single algorithm capable of deciding every formula of First-Order Logic. Incompleteness, by contrast, concerns the deductive limitations of particular formal systems sufficiently powerful to express Arithmetic.

Before Church and Turing gave a negative solution to the Decision Problem, Gödel’s results had already profoundly transformed expectations surrounding Hilbert’s Program.

Recommended Reading

– Hilbert, D. and Ackermann, W. (1928). Grundzüge der theoretischen Logik.

– Behmann, H. (1922). Beiträge zur Algebra der Logik, insbesondere zum Entscheidungsproblem.

– Church, A. (1936). “A Note on the Entscheidungsproblem.”

– Turing, A. M. (1936). “On Computable Numbers, with an Application to the Entscheidungsproblem.”