 The elimination of quantifiers became a main method in mathematical logic to prove decidability, and proving decidability was stated as the main problem of mathematical logic in Hilbert and Ackermann (1928)—this goal was dropped in subsequent editions because of the famous undecidability result of Church and Turing.