Models of arithmetical theory R + induction in which successor is not injective

Question

Consider the arithmetical theory sometimes denoted by $\mathsf{R}$. The non-logical vocabulary of $\mathsf{R}$ consists of '$0$', '$S$', '$+$' and '$\times$'. The axioms of this theory are all true instances of the following schemata:

$\overline{m}+\overline{n}=\overline{k}$

$\overline{m}\times \overline{n}=\overline{k}$

$\overline{m}\neq \overline{k}$

$\forall x\,(x\leq \overline{n}\rightarrow x=\overline{0}\vee\ldots\vee x=\overline {n})$

$\forall x\, (x\leq \overline{n}\vee\overline{n}\leq x)$

where $\overline{m}$ is the standard numeral for $m$ (i.e. '$0$' preceded by $m$-many occurrences of '$S$') and $x\leq y$ is defined in the standard way e.g. $\exists z\,(x+z=y)$.

Let $\mathsf{R}^+$ be the theory that results from adding all instances of (first- or second-order) induction to $\mathsf{R}$.

There are some quantified statements that we can prove now, e.g. $\forall x\,(x\neq 0\rightarrow \exists y\,(x=S(y)))$.

However, I'd assume that there are many general claims that still can't be proved, e.g. $\forall x\forall y\,(x+y=y+x)$. Indeed, I’d assume that one cannot even prove the injectivity of the successor function.

Question: Assuming this is correct, how can I produce a (simple) model for $\mathsf{R}^+$ + ''Successor is not injective''? What do such models look like, i.e. how do you define the successor function on the domain of such models?

Specifically, I wonder what such models look like if we embed $\mathsf{R}$ into a deduction system for "second-order logic", i.e. if we add quantifiers binding predicate places and comprehension axioms.

Answer 1

I don't have a general classification of this kind of models, but it is rather easy to construct quite a lot of models with this property.

For example (for first-order variant of your system), consider any non-standard model $\mathfrak{M}$ of $\mathsf{PA}$ (or even $\mathsf{I}\Delta_0$) and a non-standard number $a\in \mathfrak{M}$. Now let us define model $\mathfrak{N}=\mathfrak{M}\upharpoonright [0,a]$ to be the model whose domain is the interval $[0,a]\subset\mathfrak{M}$, the interpretation of successor is $S^{\mathfrak{N}}(x)=\min^{\mathfrak{M}}(S^{\mathfrak{M}}(x),a)$, the interpretation of addition is $x+^{\mathfrak{N}}y=\min^{\mathfrak{M}}(x+^{\mathfrak{M}}y,a)$, and the interpretation of multiplication is $x\times^{\mathfrak{N}}y=\min^{\mathfrak{M}}(x\times^{\mathfrak{M}}y,a)$. Using $\mathfrak{M}$-induction it is fairly easy to see that $\mathfrak{N}$ is a model of induction.

If you want to have a model of second-order variant of your system $\mathsf{R}^+$ with full scheme of comprehension, then it could be achieved by enhancing $\mathfrak{N}$ by all the subsets of $[0,a]$ coded in $\mathfrak{M}$ (i.e. all $A_u=\{b\in [0,a]\;:\; \mathfrak{M}\models p_{b}| u\}$, for $u\in \mathfrak{M}$; here $p_b$ is the $b$-th prime number). However then it is not enough for $\mathfrak{M}$ to be a model of $\mathsf{I}\Delta_0$ and we need to require it to be at least a model of $\mathsf{EA}$.