 It is worth noting that epsilon terms are nondeterministic.  For example, in a language with constant symbols \(a\) and \(b\), \(\varepsilon x (x = a \vee x = b)\) is either \(a\) or \(b\), but the calculus leaves it entirely open as to which is the case. One can add to the calculus a schema of extensionality, \[ \forall x (A(x) \leftrightarrow B(x)) \rightarrow \varepsilon x A = \varepsilon x B \] which asserts that the epsilon operator assigns the same witness to equivalent formulae \(A\) and \(B\). For many applications, however, this additional schema is not necessary.