ABSTRACT
The epsilon substitution method is based on the language with epsilon terms exF[x], read as “an x satisfying the condition F[x]”. In number-theoretic con texts it is often interpreted as the least x satisfying F[x]. The main axioms of the corresponding formalism are critical formulas
F[t] F[exF[x]] (1)
Hilbert’s epsilon substitution method for a given finite system E of critical formulas generates substitutions of numerals for closed epsilon-terms. The initial substitution So is identically 0. At every stage only a finite number of epsilonterms are assigned non-zero values. If substitutions So,. . . , Sz are already gener ated, and St is not yet a solving substitution (satisfying all critical formulas in E), then S/+i is found as follows. Fix appropriate ordering of the critical formulas (1) and take the first formula in this ordering which is false under S/, i.e., for which S^T7]/]) = true, Si(F[sxE]) = false. Set
S/+i(exF) = (the least n < t) (S/CF[h]) = true) drop the values of higher rank and preserve remaining values.
