 Turing introduced his thesis in the course of arguing that the Entscheidungsproblem, or decision problem, for the functional calculus—also known as the first-order predicate calculus—is unsolvable. This problem was first posed by David Hilbert (Hilbert and Ackermann 1928). As explained by Turing (1936: 84), Hilbert’s Entscheidungsproblem is this: Is there a general (effective) process for determining whether a given formula A of the functional calculus is provable?