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 2010 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 2010 at 14:18
@Gerald: isn't your second construction 'redundant' (some numbers are multiply represented) so that you would need to take a quotient? Yes, that is direct enough. – Jacques Carette Jun 22 2010 at 14:33
0 (zero), S (successor) , P (predecessor) Add the axioms PS(x)=SP(x)=x. – Kaveh Aug 1 2010 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 2011 at 14:17

There is a paper here http://www.denison.edu/academics/departments/mathcs/fressola_paper.pdf 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 2011 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 2011 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 2011 at 0:40
OK, sorry, I missed that comment. – Valerio Capraro Nov 7 2011 at 7:08

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.

-

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 2011 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 2011 at 15:57

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.

-