If we remove the axiom that zero doesn't have a predecessor, and stipulate that every natural number has a predecessor, and that no number is the successor of itself. And keep all other axioms of $\small \sf PA$, and introduce a new primitive relation symbol $``<"$ to signify *strictly smaller than relation*, and axiomatize that each $n^{th}$ successor of zero [for a meta-theoretic $n$] is strictly smaller than its successor, and that $<$ is asymmetric and transitive.


Formally this is the first order theory with axioms of:


axioms of first order $\small \sf PA$ minus $\not \exists x (S(x)=0)$ plus:


1. $\forall x \exists y: S(y)=x$
2. $S(x) \neq x$


Define recursively: 
$S\_0(0) = 0 \\ S\_{i+1}(0)=S(S\_i(0))$


3. For $n=1,2,3,....\\ S\_n(0) < S\_{n+1}(0)$
4. $x < y \to \neg \ y < x$
5. $ x < y < z \to x < z$


This is what I term as $\small \sf cyclic \ PA$ or $\small \sf cPA$



> 
> Question: is there an interpretation of $\small \sf cPA$ in $\small \sf PA$?
> 
> 
> 



Is cyclic PA interpretable in PA?
The theory cPA is interpretable already in Robinson’s theory $R$ by a result of Albert Visser [1], because it is recursively axiomatized and *locally finitely satisfiable*, meaning that every finite subtheory of cPA has a finite model. Indeed, a finite subtheory of cPA only mentions finitely many axioms 3, hence it is satisfied for sufficiently large $n\in\mathbb N$ in the model $(\{0,\dots,n-1\},0,S,{+},{\cdot},{<})$, where the arithmetic operations are computed modulo $n$.


An explicit interpretation of cPA in PA (or even in $I\Delta\_0$, which is itself well-known to be interpretable in $Q$) can be constructed as follows. First, PA interprets its own extension $\mathrm{PA}+\phi$ which proves the existence of a nonstandard definable element $a$: for example, we may take $\phi=\neg\mathrm{Con\_{PA}}$, and let $a$ be the least code of a proof of contradiction in PA. Then we interpret cPA by making the domain of interpretation be the interval $\{x:x<a\}$ with the induced ordering, and operations computed modulo $a$.


**Reference:**


[1] Albert Visser: *Why the theory R is special*. In: Foundational
 Adventures: Essays in Honor of Harvey M. Friedman (N. Tennant, ed.),
 Tributes vol. 22, College Publications, London, 2014. LGPS preprint no. [279](https://dspace.library.uu.nl/handle/1874/34945).


