Return to Question

My first idea on how to do this would be to replace the axiom $\not\exists x,\ Sx=0$ by $\forall x,\ SPx=PSx=x$ and defining $-1=P0$, $-2=PP0$, etc. and adjusting the addition and multiplication axioms accordingly (that is $\forall xy,Px+y=P(x+y)$, etc.)

The induction axioms may be extended to decreasing sequences (intuitively, if $\phi$ holds for $x_0$ and $\phi(x)\to\phi(Px)$ then $\phi$ holds for all numbers less than $x_0$ but I don't know how to formalize it, since $\leq$ is not defined).

Is this the canonical way to do it (if so, what is it called) or is there a problem I haven't noticed (if so, what would be the "right way")?

My first idea on how to do this would be:

1. $0\in\mathbf Z$
2. $\forall x\in\mathbf Z,Sx\in\mathbf Z\land Px\in\mathbf Z$
3. $P$ and $S$ are injective
4. $\forall x\in\mathbf Z,PSx=SPx=x$
5. some induction axiom that holds for decreasing sequences as well (intuitively, if $\phi$ holds for $x_0\in\mathbf Z$ and $\forall x\in\mathbf Z,\phi(x)\to\phi(Px)$ then $\phi$ holds for all numbers less than $x_0$)
6. addition (with the two standard axioms $\forall x\in\mathbf Z,x+0=x$ and $\forall x,y\in\mathbf Z,Sx+y=S(x+y)$ and an extra axiom $\forall x,y\in\mathbf Z,Px+y=P(x+y)$)
7. multiplication

defining $-1=P0$, $-2=PP0$, etc.

Is this the canonical way to do it (if so, what is it called) or is there a problem I haven't noticed (if so, what would be the "right way")?

My first idea on how to do this would be to replace the axiom $\not\exists x,\ Sx=0$ by $\forall x,\ SPx=PSx=x$ and defining $-1=P0$, $-2=PP0$, etc. And the induction axioms may be extended to decreasing sequences (intuitively, if $\phi$ holds for $x_0$ and $\phi(x)\to\phi(Px)$ then $\phi$ holds for all numbers less than $x_0$ but I don't know how to formalize it, since $\leq$ is not defined).

Is this the canonical way to do it (if so, what is it called) or is there a problem I haven't noticed (if so, what would be the "right way")?

My first idea on how to do this would be to replace the axiom $\not\exists x,\ Sx=0$ by $\forall x,\ SPx=PSx=x$ and defining $-1=P0$, $-2=PP0$, etc. and adjusting the addition and multiplication axioms accordingly (that is $\forall xy,Px+y=P(x+y)$, etc.)

The induction axioms may be extended to decreasing sequences (intuitively, if $\phi$ holds for $x_0$ and $\phi(x)\to\phi(Px)$ then $\phi$ holds for all numbers less than $x_0$ but I don't know how to formalize it, since $\leq$ is not defined).

Is this the canonical way to do it (if so, what is it called) or is there a problem I haven't noticed (if so, what would be the "right way")?

My first idea on how to do this would be to replace the axiom $\not\exists x,\ Sx=0$ by $\forall x,\ SPx=PSx=x$ and defining $-1=P0$, $-2=PP0$, etc. And the induction axioms may be extended to decreasing sequences.

Is this the canonical way to do it (if so, what is it called) or is there a problem I haven't noticed (if so, what would be the "right way")?

My first idea on how to do this would be to replace the axiom $\not\exists x,\ Sx=0$ by $\forall x,\ SPx=PSx=x$ and defining $-1=P0$, $-2=PP0$, etc. And the induction axioms may be extended to decreasing sequences (intuitively, if $\phi$ holds for $x_0$ and $\phi(x)\to\phi(Px)$ then $\phi$ holds for all numbers less than $x_0$ but I don't know how to formalize it, since $\leq$ is not defined).

Is this the canonical way to do it (if so, what is it called) or is there a problem I haven't noticed (if so, what would be the "right way")?