 Suppose we wish to show that the system above is consistent; in other words, we wish to show that there is no proof of the formula \(0 = 1\). By pushing all substitutions to the axioms and replacing free variables by the constant 0, it suffices to show that there is no propositional proof of \(0 = 1\) from a finite set of closed instances of the axioms. For that, it suffices to show that, given any finite set of closed instances of axioms, one can assign numerical values to terms in such a way that all the axioms are true under the interpretation. Since the arithmetical operations \(+\) and \(\times\) can be interpreted in the usual way, the only difficulty lies in finding appropriate values to assign to the epsilon terms.