 Substitution and the notions of free and bound variable, are defined in the usual way; in particular, the variable \(x\) becomes bound in the term \(\varepsilon x A\). The intended interpretation is that \(\varepsilon x A\) denotes some \(x\) satisfying \(A\), if there is one. Thus, the epsilon terms are governed by the following  axiom (Hilbert’s “transfinite axiom”): \[ A(x) \rightarrow A(\varepsilon x A) \] In addition, the epsilon calculus   includes a complete set of axioms governing the classical propositional connectives, and axioms governing the equality symbol. The only rules of the calculus are the following: