Gentzen-type systems and Hilbert's epsilon substitution method. I
G. E. Mints · Studies in logic and the foundations of mathematics · 1995
This chapter discusses the Gentzen-type systems and Hilbert's epsilon substitution method. The substitution method was suggested by Hilbert within the framework of his program for the foundations of mathematics. It is a successive approximation method for finding a finite function solution of a system of equations derived from a proof in a formal system. The proof consists of the following parts: the formalization in the infinitary sequent calculus of a noneffective proof of the existence of a solution; a standard normalization proof; and a proof that the normal form after this normalization is a convergence protocol for the epsilon substitution process. The metamathematical means used in the convergence proof are the same as in other normalization proofs for the systems considered: epsilon-0 induction (on quantifier-free formulas) for first order arithmetic and Girard's method of computability predicates in the second order case. The chapter also reviews the language, and the description of the substitution method is provided.