 Even though Ackermann’s attempts at a consistency proof for second-order arithmetic were unsuccessful, they provided a clearer understanding of the use of second-order epsilon terms in the formalization of mathematics. Ackermann used second-order epsilon terms \(\varepsilon f\ A(f)\), where \(f\) is a function variable. In analogy with the first-order case, \(\varepsilon f\ A(f)\) is a function for which \(A(f)\) is true, e.g., \(\varepsilon f (x + f(x) = 2x)\) is the identity function \(f(x) = x\). Again in analogy with the first-order case, one can use second-order epsilons to interpret second-order quantifiers. In particular, for any second-order formula  \(A(x)\) one can find a term \(t(x)\) such that \[ A(x) \leftrightarrow t(x) = 1 \] is derivable in the calculus (the formula   \(A\) may have other free variables, in which case these appear in the term \(t\) as well). One can then use this fact to interpret comprehension principles. In a language with  function symbols, these take the form \[ \exists f \forall x (A(x) \leftrightarrow f(x) = 1) \] for an arbitrary formula   \(A(x)\). Comprehension is more commonly expressed in terms of set   variables, in which case it takes the form \[ \exists Y \forall x (A(x) \leftrightarrow x \in Y), \] asserting that every second order   formula, with parameters, defines a set.