We formulate epsilon substitution method for elementary analysisEA (second order arithmetic with comprehension for arithmetical formulas with predicate parameters). Two proofs of its termination are presented. One uses embedding into ramified system of level one and cutelimination for this system. The second proof uses non-effective continuity argument.

The 1-consistency of arithmetic is shown to be equivalent to the existence of fixed points of a certain type of update procedure, which is implicit in the epsilon-substitution method.