  Hilbert and his school, with Bernays, Ackermann and von Neumann as  foremost, as well as young Herbrand in France, pursued the  metamathematical study of arithmetic in the latter part of the 1920s. Hilbert developed a method for the study of consistency problems,  called the   epsilon substitution method,  to deal with the quantifiers. He felt that indirect inferences with  quantifiers in cases with an infinity of objects were the crucial  point of consistency proofs and needed a justification. Say, if the  assumption that all natural numbers have the property P  leads to an impossibility, the existence of a number with the  contrary property not-P can be inferred. The central problem was thus to justify the use of classical logic in mathematical  proofs, arithmetical ones in the first place. Ackermann was very  close to a solution towards the end of the 1920s and optimism reigned in the Hilbert school. Then, of course, the unexpected happened when  Gödel proved the impossibility of a complete formalization of  elementary arithmetic, and, as it was soon interpreted, the  impossibility of proving the consistency of arithmetic by finitary  means, the only ones judged “absolutely reliable” by  Hilbert.