 By the summer of 1920, Hilbert had formulated such an approach. First, modern mathematical methods were to be represented in formal deductive systems. Second, these formal systems were to be proved syntactically consistent, not by exhibiting a model or reducing their consistency to another system, but by a direct metamathematical argument of an explicit, “finitary” character. The approach became known as  Hilbert's program.  The epsilon calculus was to provide the first component of this program, while his epsilon substitution method was to provide the second.