(Further reading) epsilon-calculus + Herbrand's theorem

The use of epsilon calculus was considered important to look for finitistic methods of checking consistency of first-order predicate theories (such as PA, ZFC). In view of Goedel's results, this is not possible, so the study did not continue much. Herbrand's theorem is a way to utilize and reformulate results from epsilon calculus in the language of classical logic.