 For example, consider the language of arithmetic, with symbols for \(0\), \(1\), \(+\), \(\times\), \(\lt\). Along with quantifier-free axioms defining the basic symbols, one can specify that the epsilon terms \(\varepsilon x A(x)\) picks out the least value satisfying  \(A\), if there is one, with the following axiom: \[ \tag{*} A(x) \rightarrow A(\varepsilon x A(x)) \wedge \varepsilon x A(x) \le x \]   The result is a system that is strong enough to interpret first-order (Peano) arithmetic. Alternatively, one can take the epsilon symbol to   satisfy the following axiom: \[ A(y) \rightarrow A(\varepsilon x A(x)) \wedge \varepsilon x A(x) \ne y + 1.  \]