At the 1928 International Congress of Mathematicians, David Hilbert posed the Entscheidungsproblem: is there an algorithm that, given a first-order logic formula, decides whether it is valid? It was the climax of his formalist program.
The question forced a rigorous definition of an “effective procedure.” That definition—still unsettled in 1928—arrived with Church and Turing around 1936 and showed there is no such universal decider.
For AI history, the episode matters because it turns reasoning into an algorithmic object of study: first fix the model of computation; then ask which problems are decidable or learnable.
