# Direct construction of the integers

Is there a direct construction of the integers which does not involve taking any quotients? I am of course aware of the usual construction. I am also aware of the nice axiomatic characterization of the integers.

I am most interested in a direct construction. I am sure that one could probably use a disjoint union of $\mathbb{N}$ and $\mathbb{N}^{+}$ to construct $\mathbb{Z}$. But this involves 2 intermediate constructions (as well as dealing with cases).

Edit: by direct construction, I mean something like the Peano construction for $\mathbb{N}$, seen as the inductive type built from $0$ and $\mathit{succ}$. Then one also constructs the operations of addition, multiplication, etc. Another way to think of it: suppose you wanted to have a datatype of 'integers' in a lambda calculus which only allows inductive constructions and no quotients, how would you do it?

-
The free group on one generator? Or do you want to define multiplication, as well? Maybe you should provide an example of a "direct" construction of something else to show what you have in mind. –  Gerald Edgar Jun 22 '10 at 14:13
Strings of symbols, from a three-letter alphabet (representing digits 0, 1, -1; thought of as base 3 expansions). All but finitely many digits must be zero. Define operations essentially as in grade-school. Is that what you want for "direct"? I took balanced ternary, since you don't want to start with positive integers... –  Gerald Edgar Jun 22 '10 at 14:18
0 (zero), S (successor) , P (predecessor) Add the axioms PS(x)=SP(x)=x. –  Kaveh Aug 1 '10 at 7:33
Could you explain your motivation? Are you trying to get an efficient implementation of the integers, or something that works well in a proof assistant, or something that is mathematically elegant, or what? –  Andrej Bauer Nov 7 '11 at 14:17
In that case, I would go for two-level inductive definition, followed by lemmas that show the thing has the correct universal property. Then you just keep proving everything from the universal property. Which leads to teh natural conclusion that you shouldn't really worry about how the integers are constructed, but rahter than what they are. Your proofs should not rely on any particular construction of the integers. That's my opinion. –  Andrej Bauer Nov 8 '11 at 10:49

Informally speaking, taking the limit of two's complement as the number of bits goes to $\infty$, the integers are just the eventually constant binary sequences (which are naturally represented by finite binary sequences). For this to work, said sequences must start with the least significant bit, i.e., $1001011\overline{0}$ is interpreted as $2^0+2^3+2^5+2^6$ and $1001010\overline{1}$ is interpreted as $2^0+2^3+2^5-2^7$. The arithmetic and ordering of these strings is natural (and efficient for microprocessors when we restrict from $\mathbb{Z}$ to, say, $\{-2^{63},\ldots,2^{63}-1\}$).

The above can be reinterpreted as the following less direct construction. If $R$ is the inverse limit of rings $\lim_{\infty\leftarrow n}\mathbb{Z}/2^n\mathbb{Z}$, then the diagonal map $\Delta\colon\mathbb{Z}\rightarrow R$ given by $m\mapsto \lim_{\infty\leftarrow n}(m\mod 2^n)$ is an injective ring homomorphism. [Edit: The image is characterized as the set of $\vec x\in R$ for which the truth value of $x(n+1)=x(n)$ is eventually constant.] Moreover, the ordering of $\mathbb{Z}$ is coded via $m\geq 0\Leftrightarrow(m\mod 2^n: n\in\mathbb{N})$ is eventually constant.

Update: I couldn't resist the temptation to write a functional programming implementation.

-

You could try base -2 representations, also called negabinary strings. These are finite strings drawn from the alphabet $\{ 0, 1\}$, starting with 1 (except when zero or empty, depending on your choice of convention), where we weight places by powers of $-2$. You have unique representations, and reasonably straightforward arithmetic operations.

-

There is a paper by Fresola here Integer Construction by Induction that seems to do what you want to achieve.

-
It definitely answers the question that I asked. I guess I really wanted to ask for the result to have a more natural ordering. More like balanced ternary. –  Jacques Carette Nov 6 '11 at 13:43

Is it not enough to modify Peano's construction? An idea (which is different from the onw linked by Iii) might be the following: Peano's construction makes use a function $succ(n)$ which verify the classical properties:

1. There is no $n$ such that $0=succ(n)$
2. $succ(n)=succ(m)$ implies $n=m$
3. If $0\in A$ and $succ(n)\in A$ for all $n\in A$, then $A=\mathbb N$

Maybe it is possible characterize $\mathbb Z$ making use of two (different) functions, $prec(\cdot)$ and $succ(\cdot)$, related by $prec(succ(n))=succ(prec(n))=n$. Of course, now the first property cannot be true, the second property above has to be required for both $prec$ and $succ$ and, finally, the third property has to be replaced with the following

Induction on $\mathbb Z$: If $A\subseteq Z$ contains at least one element and, moreover, for any $a\in A$ one has $prec(a),succ(a)\in A$, then $A=\mathbb Z$.

Should work.

-
This seems to be the same as what Kaveh suggested in a comment on the question. The OP objected there that the axiom prec(succ(n)) = succ(prec(n)) = n induces a quotient. That is, the integers will not be simply the terms built from succ, pred, and 0 but rather equivalence classes of such terms. –  Andreas Blass Nov 6 '11 at 23:38
Andreas is correct: I was looking for a quotient-free construction. And axioms 1-3 above are really another way of stating Goguen's "no junk, no confusion" axioms. –  Jacques Carette Nov 7 '11 at 0:40
OK, sorry, I missed that comment. –  Valerio Capraro Nov 7 '11 at 7:08

The group $\mathbf{Z}$ is the group of differences of the monoid $\mathbf{N}$, and the ring $\mathbf{Z}$ is the ring of endomorphisms of the (commutative) group $\mathbf{Z}$.

-
This is the usual construction, right? –  Martin Brandenburg Aug 16 '13 at 14:49
What's a "group of differences"? The obvious constructions require a quotient. –  James Cranch Aug 16 '13 at 15:29
Where "quotient" involves "equivalence" rather than a "division" :-) –  Wlodzimierz Holsztynski Aug 18 '13 at 4:21

(was a comment, now an answer)...

Strings of symbols, from a three-letter alphabet (representing digits 0, 1, -1; thought of as base 3 expansions). All but finitely many digits must be zero. Define operations essentially as in grade-school. Is that what you want for "direct"? I took balanced ternary, since you don't want to start with positive integers...

-

I would say: the free group on one element. I guess you can translate this into a series of first-order axioms. Notice that multiplication comes for free as composition between automorphisms of the group with itself.

Addendum: Prompted by the comment below, I am not thinking about the usual description of the free group through a chain of $1$'s and $-1$'s but on the universal property.

Let me give some specifics. A group is a tuple $(G,m,e,i)$ with $G$ a set, $m \colon G \times G \to G$ a map $e \in G$ and $i \colon G \to G$ satisfying certain commutativities that amount to the defining properties of group (associativity, $e$ is the neutral element and $i(g)$ is the inverse of the element $g \in G$). A free group in one element is such a tuple $(F, \dot , 1, op)$ satisfying that for any choice of a $g \in G$ from a group $(G,m,e,i)$ there is one and only one homomorphism $(F, \dot , 1, op) \to (G,m,e,i)$ taking $1$ to $g$. I propose to translate this description into a series of first order formulas, that was my suggestion.

Addendum 2: I have just realized that this way the description is second-order.

-
But this still has quotients (eg $xy^{-1}y=x$) which is what the OP was trying to avoid. –  Richard Rast Nov 7 '11 at 13:45
@Richard Rast. Thanks for your comment. I didn't notice the first comment in the question either. However I wonder if there is a description of the free group that does not go through a quotient, something using the universal property. –  Leo Alonso Nov 7 '11 at 15:57
@S.Carnahan, thank you for pointing to Gerald Edgar and his $(-1\ 0\ 1)$ construction. Sorry for overlooking it at the time. –  Wlodzimierz Holsztynski Aug 18 '13 at 4:04
The $(-1\ 0\ 1)$ portion of my question got removed by me, it got replaced by the original answer by Gerald Edgar (got copied by him from his own earlier comment). –  Wlodzimierz Holsztynski Aug 19 '13 at 2:03