# Do these axioms fully describe the integers?

Here, I use Peano-like axioms to describe the set of integers $Z$. They are based on two successor functions, each starting with a common point of $0$, and a principle of induction for the integers.

Let $Z$, $Pos$, $Neg$, $s$, $s'$ and $0$ be such that:

$Pos\subset Z$

$Neg\subset Z$

$Z=Pos\cup Neg$ (edit)

$\forall x (x\in Pos \wedge x\in Neg \leftrightarrow x=0)$

$s:Pos\rightarrow Pos$

$s$ is injective

$s':Neg\rightarrow Neg$

$s'$ is injective

$\forall x\in Pos (s(x)\neq 0)$

$\forall x\in Neg (s'(x)\neq 0)$

$\forall m ((0\in m\wedge \forall x\in Pos (x\in m\rightarrow s(x)\in m) \wedge \forall x\in Neg (x\in m\rightarrow s'(x)\in m))\rightarrow \forall x\in Z (x\in m))$

Note that, contrary to the usual convention, I have had to include $0$ in both sets $Pos$ and $Neg$.

Lemma: $0\in Z, Pos, Neg$

See my follow-up below

-
The usual construction seems much simpler to me. It defines an integer as a pair $(m, n)$ of natural numbers, with $(a,b) = (c,d)$ whenever $a+d = c+b$. This is simpler because it handles 0 uniformly, instead of making it a strange special case, and because it makes positive and negative the same kind of thing. One can define $(a,b) + (c,d)$ easily as $(a+c, b+d)$, without having to do separate definitions for positive and negative integers. In your system, you'll have to handle several separate cases depending on whether you are adding positive to positive, positive to negative, etc. –  MJD Jan 15 '13 at 18:00
@MJD Your construction is simpler only when you describe informally like this. Note that, for the equality of order pairs, we usually have $(a,b)=(c,d)\leftrightarrow a=c \wedge b=d$. –  Dan Christensen Jan 15 '13 at 18:17
Have fun defining addition. –  MJD Jan 15 '13 at 18:38
@MJD I have been able to construct an add function for the natural numbers starting with a version of Peano's Axioms and a single successor function s. It should be only a bit more complicated with two successor functions s and s' in this case. –  Dan Christensen Jan 15 '13 at 20:31

Yes, this characterizes the integers as long as the quantifiers on subsets range over all subsets. If you just take the axioms you have for Pos, these give Peano's axioms, which uniquely capture the natural numbers up to isomorphism in full second-order semantics. The same it true for Neg. Thus the overall structure for these axioms will be the integers, up to isomorphism.

Contrary to some claims, it is not very hard to define addition. First, there is a canonical semigroup isomorphism between (Pos, $s$) and (Neg, $s'$) preserving $0$. So this gives a notion of $-x$ for each $x$. Now we only have to define addition for positive numbers, which is described on the Wikipedia article, and then we use the negation operation to define addition for arbitrary integers.

-
Could you please elaborate a little on addition? I agree that defining addition of negative integers will look very similar to defining it for positive integers. But with the structure that OP has, I think mixing the two will yield a confusing mess. How does one calculate ${}^-3 + 5$ in this system? –  MJD Jan 15 '13 at 19:32
@MJD: we can emulate the ordered pair construction to define addition without mentioning pairs. To add $x$ and $y$, imagine $x$ is the form $(a,0)$ or $(0,a)$, and $y$ is in the form $(b,0)$ or $(0,b)$. Then the sum will be of the form $(c,0)$, $(0,d)$, or $(c,d)$. In the first case the answer is $c$, in second case it is $-d$, and in the third case the answer is $c - d$, which can be defined in two cases. If $c > d$ then $c - d$ is the unique positive $x$ with $x + d = c$, otherwise it is negative of the unique $y$ with $c + y = d$, and these only refer to addition of positive numbers. –  Carl Mummert Jan 15 '13 at 20:38
That is significantly more complicated than the definition with pairs, and it depends on defining $>$ first, which the pairs definition doesn't. I only claimed that a definition in this system would require multiple cases to treat addition of positive and negative number as separate cases, and that is exactly what you did. –  MJD Jan 15 '13 at 23:50
@MJD: the same problem will occur with pairs as soon as we eliminate the equivalence relation by putting each pair in standard form $(c,0)$ or $(0,d)$. In other words the pairs version avoids cases only by avoiding the actual equality relation. –  Carl Mummert Jan 16 '13 at 3:01

It seems that you are attempting to describe a second order theory such that, up to isomorphism, all models are the integers.

While your formulation is not entirely clear I think it can, with a bit more work, be turned into a finite list of second order axioms that will do the job.

-
There are only 11 axioms here. (I added one. See edit.) –  Dan Christensen Jan 15 '13 at 16:24
Now 12. (See edit) –  Dan Christensen Jan 15 '13 at 18:19
Back to 11! $0\in Z$ is derivable from the other axioms. –  Dan Christensen Jan 15 '13 at 18:50

This has a model in the naturals. Take $Z$ to be the naturals, $Pos$ to be the evens, $Neg$ to be the odds plus 0. Define $s$ to be $+2$ and $s'$ to be $+2$ except $s'0=1$.

-
Having a model in the naturals is not a problem. –  André Nicolas Jan 15 '13 at 7:21
@AndréNicolas.Oops, that last comment of mine, deleted, shows it is before first-espresso-of-the-day. Yes it is second order, which was indeed what I was originally assuming. Anyway, what's missing then is something that distinguishes the order structure of the integers. –  Peter Smith Jan 15 '13 at 8:02
@PeterSmith I was trying to avoid an order structure at this level. Of course, you should be able construct an add function and define $$a\leq b\leftrightarrow \exists c\in Pos (a+c=b)$$ –  Dan Christensen Jan 15 '13 at 16:20
@DanChristensen But you haven't (yet) defined addition ... –  Peter Smith Jan 15 '13 at 16:36
I am working on it. Again, I think you should be able to construct the add function from these axioms (using Cartesian product, power set and subset rules). Just added another axiom (see edit). 12 now. –  Dan Christensen Jan 15 '13 at 17:53

Follow-up

After much tinkering, I have settled on the following Peano-like axioms for the integers:

Let $Z, L, R, 0, s$ be such that:

$R\subset Z$, the non-negative integers (right)

$L\subset Z$, the non-positive integers (left)

$Z=R\cup L$

$\forall x (x\in R \wedge x\in L \leftrightarrow x=0)$

$s: Z\rightarrow Z$, a bijection

$\forall x (x\in R \rightarrow s(x)\in R)$

$\forall x (x\in L \rightarrow s^{-1}(x)\in L)$

$\forall x (x\in R \rightarrow s(x)\neq 0)$

$\forall x (x\in L \rightarrow s^{-1}(x)\neq 0)$

$\forall P ((P\subset Z \wedge 0\in P\wedge \forall x (x\in P\rightarrow s(x)\in P) \wedge \forall x (x\in P\rightarrow s^{-1}(x)\in P) ) \rightarrow Z\subset P)$

-