#### Supplement to The Church-Turing Thesis

## The Rise and Fall of the *Entscheidungsproblem*

- A. Stating the
*Entscheidungsproblem* - B. Why the problem mattered
- C. Partial solutions
- D. Negative vibes
- E. The Church-Turing result
- F. Aftermath

### A. Stating the *Entscheidungsproblem*

Turing gave two formulations of what he called “the Hilbert
*Entscheidungsproblem*” (1936 [2004: 84, 87]):

[Is there a] general process [and a few paragraphs later, he emphasizes “general (mechanical) process”] for determining whether a given formula \(A\) of the functional calculus K is provable

and:

[Is there a] machine [Turing machine] which, supplied with any one \(A\) of these formulae, will eventually say whether \(A\) is provable.

Given Turing’s thesis, the two formulations are equivalent.

Church stated the *Entscheidungsproblem* more generally:

By the

Entscheidungsproblemof a system of symbolic logic is here understood the problem to find an effective method by which, given any expressionQin the notation of the system, it can be determined whether or notQis provable in the system. (Church 1936b: 41)

While Turing and Church both formulated the *Entscheidungsproblem* in
terms of determining whether or not a formula is *provable*,
Hilbert and Ackermann had formulated it in terms of *universal
validity* (“*allgemeingültigkeit*”):

The

Entscheidungsproblemis solved once we know a procedure that allows us to decide, by means of finitely many operations, whether a given logical expression is universally valid or, alternatively, satisfiable. (Hilbert & Ackermann 1928: 73)

A universally valid formula of the functional calculus (e.g., \((x)(Fx
\lor \neg Fx)\) or, in modern notation, \(\forall x(Fx \lor \neg
Fx)\)) must contain neither free variables nor individual constants,
and is such that a true assertion results no matter which replacements
(of suitable adicity) are made for the formula’s predicate
symbols, and no matter which objects are allocated to its variables
(Hilbert & Ackermann 1928: 72–73). In the case of a
satisfiable formula (e.g., \((Ex)Fx\) or, in modern notation,
\(\exists xFx\)) there must be *at least one* way of replacing
its predicate symbols and of allocating objects to its variables so
that a true assertion results. Universal validity and satisfiability
are related as follows: \(A\) is universally valid if and only if
\(\neg A\) is not satisfiable (1928: 73). In the above quotation,
therefore, Hilbert and Ackermann are presenting two different but
equivalent forms of the *Entscheidungsproblem*, one employing the
concept of universal validity (or simply validity, as we would say
today) and the other the closely related concept of satisfiability.
The hunt was on for what they called “a determinate, finite
procedure” (1928: 17) for deciding, of any given formula \(A\)
of the functional calculus, whether or not \(A\) is universally valid,
or, equivalently, for deciding whether or not \(\neg A\) is
satisfiable.

Turing’s and Church’s provability formulation of the
*Entscheidungsproblem* and the Hilbert-Ackermann formulation in terms of
validity are in fact logically equivalent, as Church noted in 1936
(1936b: 41). This equivalence is a consequence of Gödel’s
proof that (where \(A\) is any formula of the functional calculus) if
\(A\) is universally valid then \(A\) is provable in the calculus.
(The proof was presented originally in Gödel’s 1929
doctoral dissertation and then published as Gödel 1930.)
Nevertheless, the provability version of the *Entscheidungsproblem* is
arguably superior, since it asks a question about a specific axiom
system, as do the allied problems of consistency and completeness. In
modern treatments, the problems of consistency, completeness and
decidability for an axiom system lie at the heart of proof theory, the
area of modern logic founded by Hilbert.

In 1928, Hilbert and Ackermann were certainly aware of the provability formulation (1928: 86, and see below) but they gave the validity formulation the starring role. It was von Neumann who emphasized the provability formulation, calling the process of proof the “real heart of mathematics” (von Neumann 1927: 10).

### B. Why the problem mattered

Why was it that the *Entscheidungsproblem* was regarded as “the
main problem of mathematical logic” and “the most general
problem of mathematics”? There were fundamentally two
reasons.

#### B.1 A “philosophers’ stone”

In his turn-of-the-century Paris lecture, Hilbert explained the idea
of *axiomatizing* a subject-matter and using provability from
the axioms as the touchstone of truth:

When we are engaged in investigating the foundations of a science, we must set up a system of axioms which contains an exact and complete description of the relations subsisting between the elementary ideas of that science…. [N]o statement within the realm of the science whose foundation we are testing is held to be correct unless it can be derived from those axioms by means of a finite number of logical steps. (Hilbert 1900: 264 [trans. 1902: 447])

He also famously said in his lecture that there is “no
*ignorabimus*” in mathematics—there is nothing that
we shall not know (Hilbert 1900: 262). It was a phrase he would often
use to express his “conviction of the solvability of every
mathematical problem” (Hilbert 1900: 262 [trans. 1902: 445]).
Thirty years later he reiterated the same standpoint, in a valedictory
lecture in Königsberg:

[I]n my opinion, there is no such thing as an unsolvable problem. On the contrary, instead of foolish ignorabimus, our slogan is: We must know, We will know. (Hilbert 1930b: 963)

It was Hilbert’s great invention, proof theory, that would, he thought, supply the basis for answering all “meaningful questions”:

[O]n the basis of the proof theory I have outlined, every fundamental question can be answered in a way that is unambiguous and mathematically precise. (Hilbert 1930a: 8, 9)

However, proving a statement in an axiom system can be a tricky matter. Suppose the mathematician fails to discover a derivation of the statement from the axioms, what follows then? The failure could be because the statement is indeed not provable—but, on the other hand, there might be a way to prove it that escaped the mathematician’s attention. Success in finding a proof brings certainty, whereas failure leaves us uncertain. That is why a decision method is so desirable. The method enables the mathematician to determine whether or not the statement is provable. Thinking up proofs is a serendipitous activity that involves, as Behmann put it, “inventive insight”, “creative thought”, and searching “in every direction of the compass” (Behmann 1921: 2–3 [trans. 2015: 174]). Whereas a decision method is a purely mechanical process that is guaranteed to produce a definite answer.

Herbrand wrote of the “present great ambition, the solution of
the *Entscheidungsproblem*”, saying this “would provide a
general method in mathematics” and enable us to “to decide
with certainty whether a proposition is true in a given theory”
(Herbrand 1930b: 254–255). In his 1921 lecture, Behmann had
referred to this desired general method as a
“philosophers’ stone” (“*Stein der
Weisen*”), by means of which mathematicians “would be
able to *solve every problem posed*”—or even
“delegate the work of proving mathematical theorems to
mathematical laborers” (Behmann 1921: 3–4 [trans. 2015:
175], emphasis added). Turing’s mentor Newman, familiar of
course with the work of the Hilbert group, also referred to the
solution of the *Entscheidungsproblem* as a philosophers’ stone.
Hilbert and Ackermann themselves said, in 1928:

Solving this general

Entscheidungsproblem[for the second-order functional calculus] would … enable us to decide on the provability or unprovability ofany mathematical proposition, at least in principle. (Hilbert & Ackermann 1928: 86, emphasis added)

Schönfinkel went even further. He was another member of the
Göttingen group who praised “Leibniz’s bold
conjectures” (Schönfinkel 192?: 2). (For an excellent
biographical article on Schönfinkel, see Wolfram 2021.) In an
early draft of what would become Bernays and Schönfinkel (1928),
Schönfinkel wrote of “the great *Entscheidungsproblem* of
mathematical logic” which, thanks to Hilbert, mathematicians now
had “the courage and the boldness to dare to touch”. He
described the *Entscheidungsproblem* as “the problem of
‘solving all problems’”—not just all
mathematical problems but *all* problems. Because once there is
a method for solving all mathematical problems:

thereafter everything else is indeed lightweight, once this “Gordian knot” is undone (since “the world is written in mathematical characters”). (Schönfinkel 192?: 1–2)

#### B.2 The consistency of mathematics

The second reason the *Entscheidungsproblem* was regarded as so
important was its connection with the quest for proofs of the
*consistency* of mathematical systems. A system is said to be
inconsistent if there is some statement \(A\) such that both \(A\) and
\(\neg A\) are provable from the axioms. The system is consistent if
(and only if) there is no statement for which this sorry situation is
the case.

By the early twentieth century, mathematics—until then a “paragon of reliability and truth”, Hilbert said—was in trouble (Hilbert 1926: 170, trans. in van Heijenoort 1967: 375). Its reputation had been “lost due to the paradoxes of set theory” (Hilbert 1922: 160). Hilbert explained:

[C]ontradictions appeared, sporadically at first, then ever more severely and ominously…. In particular, a contradiction discovered by Zermelo and Russell [“Russell’s paradox”] had, when it became known, a downright catastrophic effect in the world of mathematics. (Hilbert 1926: 169 [trans. 1967: 375])

Herbrand takes up the story:

One must take great care … Set theory has produced famous examples [of inconsistencies] … But there is nothing to show us that similar issues do not arise for the theories that seem to us the most finished, like arithmetic. Could it be that arithmetic is inconsistent? (Herbrand 1930b: 250–251)

“[P]roofs of consistency would be very useful to dispel lingering doubts”, wrote Herbrand (1930b: 251). Hilbert put it even more forcefully:

[T]he situation in which we presently find ourselves with respect to the paradoxes is in the long run intolerable. (Hilbert 1926: 170 [trans. 1967: 375])

Proving “the consistency of the arithmetic axioms” is “urgent”, he said—“a burning question” (Hilbert 1926: 179 [trans. 1967: 383]; Hilbert 1930a: 3). Hilbert’s overarching concern was to “re-establish mathematics’ old reputation for incontestable truth” (Hilbert 1922: 160), and he was “convinced that it must be possible to find a direct proof of the consistency of the arithmetical axioms” (Hilbert 1900: 265).

A solution to the *Entscheidungsproblem* would furnish a route to
establishing consistency: “By means of the decision method,
issues of consistency would also be able to be resolved”
(Hilbert & Ackermann 1928: 76). This is because the decision
method could be used to establish whether or not \(A\) and \(\neg A\)
are both provable—so gaining a definite answer to the question
“Is the system consistent?”. Hilbert believed that,
following the discovery of the decision method, arithmetic and
analysis would be proved consistent, thereby “establish[ing]
that mathematical propositions are indeed incontestable and absolute
truths” (Hilbert 1922: 162). Mathematics’ reputation would
be regained.

### C. Partial solutions

By the time Turing and Church engaged with the *Entscheidungsproblem*, a
number of decision methods were known for *parts* of the
functional calculus.

Besides the previously mentioned Hilbert-Bernays decision method for
the propositional calculus (and Peirce’s much less well-known
method), and also the Löwenheim method for the monadic fragment
of the functional calculus (later improved by Behmann in his 1922
paper, where it was additionally proved that the monadic fragment of
the second-order functional calculus is decidable), there were various
decision methods that succeeded providing the functional calculus
was restricted in one way or another. Bernays and Schönfinkel
(1928) showed there is a decision method when formulae containing at
most two individual variables are considered. At Cambridge, Ramsey
devised a method that worked provided existential quantifiers were
omitted from the calculus, and any universal quantifiers were stacked
one after another at the very beginning of a formula (with no negation
sign preceding any of them, and with their scope extending to the end
of the formula). Such formulae are interesting, Ramsey pointed out,
since they represent “general laws” (Ramsey 1930: 272;
Langford 1926b: 115–116). Ackermann, Bernays, Schönfinkel,
Gödel, Kálmar, and Herbrand devised methods for other
fragments of the calculus, in which only certain patterns of
quantifiers were permitted. Gödel’s 1933 paper on the
*Entscheidungsproblem* gave a summary of some of the developments.

Despite all this attention to the decision problem, no method had been
found for the full functional calculus. But according to Hilbert it
was just a matter of time. He and Ackermann emphasized that
“finding a general decision process is an as yet unsolved and
difficult problem” (1928: 77). They exuded optimism, writing
buoyantly of moving “closer to the solution of the
*Entscheidungsproblem*” (1928: 81).

### D. Negative vibes

Even in the 1920s, however, negative opinion on the solvability of the
*Entscheidungsproblem* was building. Behmann had pointed out in his 1921
lecture that, once the “philosophers’ stone” was
found, “the entirety of mathematics would indeed be transformed
into one *enormous triviality*” (Behmann 1921: 5 [trans.
2015: 175]). Some found this consequence highly unpalatable. In 1927,
Hilbert’s student Weyl insisted that “such a
philosopher’s stone has not been discovered and never will be
discovered”, and a good job too, Weyl thought, since if it were,
“Mathematics would thereby be trivialized” (Weyl 1927: 20
[trans. Weyl 1949: 24]). Then a year later, in 1928, Hardy announced
to the Cambridge mathematicians, assembled at his Rouse Ball Lecture,
that he expected no “system of rules which enable us to say
whether any given formula [is] demonstrable or not” (Hardy 1929:
16). “[T]his is very fortunate”, he continued, since if
there were such a system,

we should have a mechanical set of rules for the solution of all mathematical problems, and our activities as mathematicians would come to an end. (ibid.)

Hardy explained that his description of Hilbert’s ideas was
“based upon that of v. Neumann, a pupil of
Hilbert’s”, saying that he found von Neumann’s
exposition “sharper and more sympathetic than Hilbert’s
own” (Hardy 1929: 13–14). Hardy was referring to von
Neumann’s “Zur Hilbertschen Beweistheorie” (*On
Hilbert’s Proof Theory*), published in 1927 but completed by
the middle of 1925. Von Neumann said:

So it

seemsthat there is no way to find the general decision criterion for whether a given normal formula [i.e., a well-formed formula with no free variables] is provable. (von Neumann 1927: 11, emphasis added)

Also:

The day that undecidability lets up, mathematics in its current sense would cease to exist; into its place would step a perfectly mechanical rule, by means of which anyone could decide, of any given proposition, whether this can be proved or not. (von Neumann 1927: 12)

But how to *prove* that there is no general decision criterion?
Von Neumann confessed he did not know:

At present, of course, we cannot demonstrate this. Moreover, no clue whatsoever exists how such an undecidability proof would have to be conducted. (von Neumann 1927: 11)

Nor did he find a proof. With a hint of resignation he said in 1931
that the *Entscheidungsproblem* was “far too difficult”
(1931: 121). Four years later, in 1935, he visited Cambridge for a
term (arriving in April, a few weeks after Newman had lectured on
the *Entscheidungsproblem*) and he struck up an acquaintance with a
young mathematician who admired his work (Copeland & Fan 2023).
The young man was of course Alan Turing, who within a few months would
devise his groundbreaking proof that—just as von Neumann had
hypothesized—“It is generally undecidable whether a given
normal formula is provable or not” (von Neumann 1927: 12). Was
there discussion, during the spring of 1935, between von Neumann and
Turing (the latter already primed by Newman’s lecture) about the
*Entscheidungsproblem*—which was, after all, the main problem of
mathematical logic? Did von Neumann perhaps play a role in
Turing’s decision to take on this fundamental problem and prove
it unsolvable? These are tantalizing questions, and we may never know
for sure.

### E. The Church-Turing result

Gödel’s famous incompleteness theorems of 1931 placed
unexpected new obstacles in the way of Hilbert’s desired
consistency proof for arithmetic (Gödel 1931). Suspicion also
began to build that Gödel’s incompleteness results might
further imply the unsolvability of the *Entscheidungsproblem*. Herbrand
said cautiously:

[A]lthough at present the possibility of a solution to the

Entscheidungsproblemseems unlikely, its impossibility has not yet been proved. (Herbrand 1931a: 56)

Carnap, who took a close interest in Hilbert’s Göttingen group and had worked with Behmann (Schiemer, Zach, & Reck 2017) wrote the following about the Hilbertian idea of a “definite criterion of validity” or “decision procedure for mathematics”, using which “we could so to speak calculate the truth or falsity of every given proposition”:

[B]ased on Gödel’s latest results, the search for a definite criterion of validity for the entire system of mathematics appears hopeless. (Carnap 1935: 163–4)

But, as Herbrand noted, nobody had *proved* the
*Entscheidungsproblem* to be unsolvable. That was where Turing and
Church entered the story. Newman later summed up matters as they had
appeared at the time, before Church and Turing published their
transformational papers in 1936:

A first blow was dealt [to the “Hilbert decision-programme”] by Gödel’s incompleteness theorem (1931), which made it clear that truth or falsehood of \(A\) could not be equated to provability of \(A\) or not-\(A\) in any finitely based logic, chosen once for all; but there still remained in principle the possibility of finding a mechanical process for deciding whether \(A\), or \(\neg A\), or neither, was formally provable in a given system. (Newman 1955: 256)

Turing summed up his show-stopping result in his usual terse way: he
had shown, he said, that “the Hilbert *Entscheidungsproblem* can
have no solution” (Turing 1936 [2004: 84]). Church, also not one
to waste words, compressed his proof into a paper barely two pages
long, and concluded pithily:

The general case of the

Entscheidungsproblemof the engere Funktionenkalkül is unsolvable. (Church 1936b: 41)

In establishing this, Turing and Church showed moreover that there can be no decision method for the second-order functional calculus (where quantification is permitted over not just individuals but also over properties and relations), since the second-order calculus contains the first-order calculus as a fragment. The same applies to every other mathematical system containing the first-order calculus, such as arithmetic.

However, it is one of the great ironies of the history of logic that, all along, Gödel’s first incompleteness theorem of 1931 did in fact suffice to establish the undecidability of the functional calculus—although this was certainly not apparent at the time. More than three decades passed after the publication of Gödel’s paper before this corollary of his theorem was noted, by Davis (Davis 1965: 109; Kleene 1986: 136).

Naturally, this unnoticed implication of Gödel’s theorem does not diminish Turing’s and Church’s great achievement, which at the time broke new ground. However, in recent times their work is sometimes regarded as amounting to merely a smallish development of Gödel’s previously published results, on which Church’s and Turing’s work was supposedly based. This is particularly true of Turing. Turing, it is said, “merely reformulated Gödel’s work in an elegant way” (Schmidhuber 2012: 1638) and “recast” Gödel’s findings “in the guise of the Halting Problem” (Dawson 2006: 133). (For further discussion of these and similar views, see Copeland & Fan 2022.) In this connection, it is worth remembering the words of Kleene, who worked closely with Church and played a leading part in the development of computability theory in the 1930s. Kleene noted that

One sometimes encounters statements asserting that Gödel’s work laid the foundation for Church’s and Turing’s results

and commented:

Whether or not one judges that Church would have proceeded from his thesis to these [undecidability] results without his having been exposed to Gödel numbering, it seems clear that Turing in [“On Computable Numbers”] had his own train of thought, quite unalloyed by any input from Gödel. One is impressed by this in reading Turing [“On Computable Numbers”] in detail. (Kleene 1987: 491–2)

### F. Aftermath

What became of the *Entscheidungsproblem* after the Church-Turing
negative result?

In letters written in the wake of the result, Turing and Newman discussed the idea Newman had presented in his 1935 lecture, a machine that is able to decide mathematical problems. Turing wrote “I think you take a much more radically Hilbertian attitude about mathematics than I do”, responding to Newman’s statement that

If all this whole formal outfit is not about finding proofs which can be checked on a machine it’s difficult to know what it is about. (Turing c.1940 [2004: 215])

Turing noted that he saw no essential difference between a proof-checking machine and a proof-finding machine. He challenged Newman:

When you say “on a machine” do you have in mind that there is (or should be or could be, but has not been actually described anywhere) some fixed machine on which proofs are to be checked, and that the formal outfit is, as it were about this machine?

Turing called this an “extreme Hilbertian” position, and said:

If you take this attitude … there is little more to be said: we simply have to get used to the technique of this machine and resign ourselves to the fact that there are some problems to which we can never get the answer.

Turing rejected this attitude to mathematics, because, he said, “there is a fairly definite idea of a true formula which is quite different from the idea of a provable one”—mathematicians’ judgements about whether formulae are true can outrun the pronouncements of the Hilbertian machine. Turing continued in his letter:

If you think of various machines I don’t see your difficulty. One imagines different machines allowing different sets of proofs, and by choosing a suitable machine one can approximate “truth” by “provability” better than with a less suitable machine … (Turing c.1940 [2004: 215])

In Turing’s opinion, that was how the debate on the
*Entscheidungsproblem* had panned out. The Hilbertians had wanted a
single decision method for the whole of mathematics—a single
computing machine or algorithm—whereas Turing showed there can
be no such thing; but he emphasized that there are, nevertheless,
different decision methods (machines) for different areas of
mathematics (see further Copeland & Shagrir 2013). In place of the
one great unsolvable decision problem, there are many lesser, but
often solvable, decision problems.

In the long aftermath of the Church-Turing result, as those rough pioneering days gave way to modern computer science, Turing’s opinion became the mainstream view: Today, computer science makes use of a multiplicity of algorithms for deciding different parts of the functional calculus and other mathematical systems.