Epsilon substitution for first- and second-order predicate logic (Q1946675)

Epsilon substitution is an approach for consistency proofs. This paper consists of two parts: first order and second order. In the first part, the author presents ``a streamlined reformulation'' of the \(\varepsilon\)-substitution procedure of \textit{D. Hilbert} and \textit{P. Bernays} [Grundlagen der Mathematik. Bd. 2. Berlin: Julius Springer (1939; Zbl 0020.19301; JFM 65.0021.02); 2nd ed. (1970; Zbl 0211.00901)]. As to the second part, it is stated, ``[as] far as the author knows, there have been no attempts to extend this approach to the second-order case''. Although there are a few results in this direction, they are about subsystems of second-order arithmetic. The author's approach is as follows: first define the set of natural numbers as the minimal set that contains zero and closed under successor. Then, mathematical induction is provable, and so \(\varepsilon\)-substitution goes exactly as in the first-order case. (As a matter of fact, in the definition of rank -- a crucial notion -- no distinction is made between first- and second-order \(\varepsilon\)-terms.) Of course, the procedure fails because of impredicativity -- the substituting term can be of higher rank. The author points out a few other difficulties. For instance, an arbitrary sequence of substitution may not terminate, even in the first-order case. He also suggests trying (seemingly) easier system like the ramified one.