Of course any model \(\mathcal{M} \models \mathsf{S}^1_2 + \exists y \neg \exists z \varepsilon(2,y,z)\) must be nonstandard. Thus not only must the domain of \(\mathcal{M}\) be infinite, but also there will exist ‘natural numbers’ in the sense of \(\mathcal{M}\) which will have infinitely many predecessors when viewed from the outside of \(\mathcal{M}\). One might thus at first think that the use of structures like \(\mathcal{M}\) to explore the consequences of strict finitism would be antithetical to its proponents.