$\phi$ is a $\exists^+_1$ formula iff it is in language of arithmetic and does not have $\forall$,$\neg$ and $\rightarrow$, therefore $I\exists^+_1$ is theory of $Q$+induction axioms for $\exists^+_1$ formula. I know that $I\exists^+_1$ has a model like $M\models I\exists^+_1$ such that:
$1.M=\mathbb{N}\cup\{\omega \}\\ 2.M\models S\omega =\omega\\ 3.M\models \omega+\omega=\omega\\ 4.M\models \omega \cdot \omega =\omega\\ 5.\forall n \in \mathbb{N}(M\models n<\omega) $
This model is interesting because it has max element $\omega$, so $M\not \models x+z=y+z\rightarrow x=y$. I want to classify other models of this theory like $M'$ such that $M'\not \models x+z=y+z\rightarrow x=y$ but I can't.
What is models of $I\exists^+_1$ is look like?(models that not satisfy $x+z=y+z\rightarrow x=y$)
Also is there any model $W\models I\exists^+_1$ ,such that $\exists a,b\in W(W\models Sa=b \wedge Sb=a)?$
Thanks
