 The difficulty in dealing with nested epsilon terms can be described as follows. Suppose one of the axioms in the proof is the transfinite  axiom \[ B(y) \rightarrow B(\varepsilon y B(y)) \] \(\varepsilon y   B(y)\) may, of course, occur in other formulae in the proof, in   particular in other transfinite axioms, e.g., \[ A(x, \varepsilon y B(y)) \rightarrow A(\varepsilon x A(x, \varepsilon y B(y)), \varepsilon y B(y)) \] So first, it seems necessary to find a correct   interpretation for \(\varepsilon y B(y)\) before we attempt to find one for \(\varepsilon x A(x, \varepsilon y B(y))\). However, there are more complicated patterns in which epsilon terms may occur in a proof. An instance of the axiom, which plays a role in determining the   correct interpretation for \(\varepsilon y B(y)\) might be \[ B(\varepsilon x A(x, \varepsilon y B(y))) \rightarrow B(\varepsilon y B(y)) \] If \(B\)(0) is false, then in the first round of the   procedure \(\varepsilon y B(y)\) will be interpreted by 0. A subsequent change of the interpretation of \(\varepsilon x A(x, 0)\) from 0 to, say, \(n\), will result in an interpretation of this instance as \(B(n) \rightarrow B\)(0) which will be false if \(B(n)\) is true. So the interpretation of \(\varepsilon y B(y)\) will have to be corrected to \(n\), which, in turn, might result in the interpretation of \(\varepsilon x A(x, \varepsilon y B(y))\) to no longer be a true formula.