 In other words, if there is any witness \(y\) satisfying \(A(y)\), the epsilon term returns a value whose predecessor does not have the same property. Clearly the epsilon term described by (*) satisfies the alternative axiom; conversely, one can check that given \(A\), a value of \(\varepsilon x (\exists z \le x A(x))\) satisfying the alternative axiom can be used to interpret \(\varepsilon x A(x)\) in (*). One can  further fix the meaning of the epsilon term with the axiom \[ \varepsilon x A(x) \ne 0 \rightarrow A(\varepsilon x A(x)) \] which   requires that if there is no witness to \(A\), the epsilon term return 0. For the discussion below, however, it is most convenient to focus on (*) alone.