Recall that the theory \(\text{I}\Delta_0\) introduced in   Section 4.5   allows us to define the graph of the exponential function \(x^y\) via a \(\Delta_0\)-formula \(\varepsilon(x,y,z)\) in the sense that \(\text{I}\Delta_0 \vdash \forall x\varepsilon(x,0,1)\) and \(\text{I}\Delta_0 \vdash \forall x \forall y \forall z(\varepsilon(x,y,z) \rightarrow \varepsilon(x,y+1,z \cdot x))\). But as we have seen, \(\text{I}\Delta_0\) does not prove the totality of the exponential function nor (as can be also be shown) does Buss’s theory \(\mathsf{S}^1_2\). From this it follows that the theory \(\mathsf{S}^1_2 + \exists y \neg \exists z \varepsilon(2,y,z)\) is proof-theoretically consistent. By the completeness theorem for first-order logic, there thus exists a model \(\mathcal{M}\) for the language of bounded of arithmetic such that \(\mathcal{M} \models \mathsf{S}^1_2 + \exists y \neg \exists z \varepsilon(2,y,z)\). But although it follows from Theorem 4.5 that all the polynomial time computable functions are defined for all inputs in \(\mathcal{M}\), there also exists an object \(a\) in the domain of \(\mathcal{M}\) satisfying \(\neg \exists z \varepsilon(2,a,z)\). And from this it follows that the expression we would conventionally write as ‘\(2^a\)’ fails to denote a value in \(\mathcal{M}\).[54]