(Finite) Models of two subtheories of Peano Arithmetic

Consider first-order theory (with identity) of Peano Artithmetic built in the language $\{S,+,\times,0\}$ and with the following set of axioms: \begin{align} \neg Sx&=0\tag{1}\\\ Sx=Sy&\rightarrow x=y\tag{2}\\\ x+0&=x\tag{3}\\\ x+S(y)&=S(x+y)\tag{4}\\\ x\times 0&=0\tag{5}\\\ x\times S(y)&=(x\times y)+x\tag{6} \end{align} plus the full induction schema.

Let $PA^{(-1)}$ be the subtheory of $PA$ (first-order Peano Arithmetic) which has all other axioms except for (1), similarly $PA^{(-2)}$ let be the subtheory without (2). It is rather easy, but nevertheless interesting, result that both this theories have finite models, $PA^{(-1)}$ even has the degenerate one-element model.

My question is: has any research been made towards characterization of class of models of the theories above? If yes, could please someone provide me with suitable information? I am particularly interested in finite models.

EDIT: Following J.D. Hamkins advice I explicitly stated the language and the axiomatization I am interested in.

-
Since there are various standard equivalent formulations of PA, which are no longer equivalent when you drop axioms, it may help to be more explicit about what the axioms of your theories are. In particular, first-order PA is usually axiomatized in the language of ordered rings, in the language with $+, \cdot, 0,1$ and $\lt$, rather than in the language with unary successor $S$. (But of course we can define $S(x)$ in that language as $x+1$.) –  Joel David Hamkins Nov 4 '12 at 13:55
I agree with Joel... As stated, without addition and multiplication, the models are easy to characterize: Models of $PA^{(-1)}$ are of the form $(X;0,S)$ where $0 \in X$ and $S:X \to X-\lbrace0\rbrace$. Models of $PA^{(-2)}$ are of the form $(X;S)$ where $S:X\to X$ is an injection (and, if desired, $0$ is any element of $X$). –  François G. Dorais Nov 4 '12 at 15:59
Following J.D. Hamkins' advice I stated explicitly what language and what axiomatization I am interested in. –  Mad Hatter Nov 4 '12 at 16:01
You should look at Leon Henkin, "On Mathematical Induction," The American Mathematical Monthly, Vol. 67, No. 4 (Apr. 1960), pp. 323-338. You might also find this interesting (in your axiomatiation, you're assuming the functionality and totality of the successor function, but these can also be removed): andrewboucher.com/papers/ga.pdf –  abo Nov 4 '12 at 18:07
@abo: Thanks for the references. –  Mad Hatter Nov 4 '12 at 19:19

Infinite models are partly classified by two theorems of $PA^{(-1,2)}$ the subtheory of $PA$ without axioms 1 or 2. Then I will describe the finite models completely.

In $PA^{(-1,2)}$ if axiom 1 fails then axiom 2 holds. For proof, express failure of axiom 1 by a constant $c$ with $S(c)=0$. Then $PA^{(-1,2)}$ proves $\forall x (c+S(x)=x)$, which implies axiom 2. In this case the numbers form a group under addition.

So if axiom 2 fails then axiom 1 holds. In that case we are in $PA^{(-2)}$ and axiom 2 fails at just one number $p$, there is an interval $[0,p]$ linearly ordered by addition, and the remaining numbers satisfy $PA^{(-1)}$ with $p$ in the role of 0.

To prove the claims in the preceding paragraph, consider the following formula $\Phi(x)$ which is meant to say successor is one-to-one up to $x$ (but so far we have not defined an order relation):

$\forall y,z,u,v (\ (y+z=x\ \&\ S(u)=S(v)=y) \rightarrow u=v)$

The usual proof of $x+y=0 \rightarrow y=0$ works in $PA^{(-2)}$ and the usual additive order relation is well defined on the set defined by $\Phi$. So $\Phi(0)$ and if axiom 2 fails there is some $p$ in $\Phi$ with successor not in $\Phi$ and the set defined by $\Phi$ is linearly ordered as an interval $[0,p]$.

Induction shows for every $x$ either $\Phi(x)$ or $\exists y (x=p+y)$ while conversely $\Phi(p+y)\rightarrow y=0$. In particular $p$ is successor to at least one number of form $p+y$.

The numbers of form $p+y$ provide an obvious interpretation of $PA^{(-1,2)}$ with $p$ in the role of 0, and this interpretation falsifies axiom 1. So it satisfies axiom 2. It interprets $PA^{(-1)}$.

Finite models of full induction are easy. Assuming no axioms for now, the list of iterated values $0,S(0),SS(0),\dots$ is finite in any finite model so the set of all the iterated values is definable (without parameters) by a finite disjunction $x=0\vee x=S(0)\vee x=SS(0)\vee \dots$ in that model. Assuming induction that set is the whole model.

That means (following Blass's comment) the $S$ series is eventually cyclic, so there are $m$ and $n > m$ with $0,S(0),\dots S^{n-1}(0)$ all distinct but $S^{n}(0)=S^m(0)$.

Now assume axioms 3--6 on $+$ and $\times$. Then all classically correct equalities between numerals (terms $S^p(0)$ for any number $p$) are provable, just as in $PA$ (but the classically false ones are not refutable). And every element of any model is named by at least one numeral of that form.

So, for any eventually cyclic $S$ series, at most one definition of $+$ and $\times$ produces a model of axioms 3--6 plus full induction. And one does, namely using standard arithmetic below $m$ and arithmetic mod $n-m$ above $m$. The extreme cases are helpful in understanding: if $m=0$ then we have arithmetic mod $n$ and a model of axioms 2--6 plus induction. If $m=n-1$ then we have arithmetic with $n-1$ as an absorbing upper bound, a model of axioms 1 and 3--6 plus induction.

To be a bit more explicit, given an $S$ series with $n$ and $m$ as above, define an equivalence relation $=_0$ by saying: $x=_0 y$ iff either $x=y$ and both are $\leq m$, or both are $\geq m$ and have $x=y$ mod $n-m$, You just have to show this is a congruence for $S,+,\times$ which is pretty direct since $S,+,\times$ are all strictly increasing in each argument, except multiplying by 0.

-
Without the successor axioms, one can imagine models that are "eventually cyclic", i.e., for some $m<n$ we have $0,S0,\dots,S^n0$ distinct but $S^{n+1}0=S^m0$. Your examples are the cases $m=0$ and $m=n$. Are you saying that the other possibilities are excluded by the addition and multiplication axioms? –  Andreas Blass Aug 7 '13 at 15:14
The structure is the quotient of the semiring $(\mathbb N,0,1,+,\cdot)$ over the congruence $x\sim y$ iff $x=y$ or $x,y>n$ and $x\equiv y\pmod{m-n}$, so it satisfies all identities (or indeed all positive sentences) valid in $\mathbb N$. –  Emil Jeřábek Aug 8 '13 at 11:26
@EmilJeřábek I add a comment to say your comment was aimed at my earlier version with just the finite models. It got me to look at models in general as quotients of non-standard models of PA, though I do not (so far) know how rigorous that can be made. –  Colin McLarty Aug 12 '13 at 2:20