 Further reading. The original sources on the epsilon-calculus and the epsilon theorems (Ackermann 1924, Hilbert &amp; Bernays 1939) remain available only in German. Leisenring 1969 is a relatively modern book-length introduction to the epsilon calculus in English. The first and second epsilon theorem are described in detail in Zach 2017. Moser &amp; Zach 2006 give a detailed analysis for the case without equality. The original proofs are given for axiomatic presentations of the epsilon-calculus. Maehara 1955 was the first to consider sequent calculus with epsilon terms. He showed how to prove the second epsilon theorem using cut elimination, and then strengthened the theorem to include the schema of extensionality (Maehara 1957). Baaz et al. 2018 give an improved version of the first epsilon theorem. Corrections to errors in the literature (including Leisenring’s book) can be found in Flannagan 1975; Ferrari 1987; and Yasuhara 1982. A variation of the epsilon calculus based on Skolem functions, and therefore compatible with first-order logic, is discussed in Davis &amp; Fechter 1991.