# Integer

The integers are the ring of non-fractional numbers:

... -3, -2, -1, 0, 1, 2, 3, ...

These are the natural numbers, with the addition of their additive inverses. In other words, the integers extend the natural numbers into an abelian group under addition.

We can construct a model for the integers. Start with the model of the natural numbers. Then construct two "flag objects", using pieces of that model:

Failed to parse (Cannot write to or create math temp directory): F_1 \equiv \{0,2\} = \{\phi,\{\phi,\{\phi\}\}\}

Failed to parse (Cannot write to or create math temp directory): F_2 \equiv \{0,3\} = \{\phi,\{\phi,\{\phi\}, \{\phi, \{\phi\}\}\}\}

Our model of the natural numbers, as laid out on the natural numbers page, consisted of the sets

Failed to parse (Cannot write to or create math temp directory): 0 \equiv \Phi = \{\}

Failed to parse (Cannot write to or create math temp directory): 1 \equiv \{0\}

Failed to parse (Cannot write to or create math temp directory): 2 \equiv \{0,1\}

Failed to parse (Cannot write to or create math temp directory): 3 \equiv \{0,1,2\}

...

We can see by inspection that F1 and F2 are not equal to any of those. We can, therefore, use the flags to tag two copies of the natural numbers. We now define the objects used in the model of the integers, shown here with primes attached, to distinguish them from the similar objects used in modeling the natural numbers:

Failed to parse (Cannot write to or create math temp directory): 0' \equiv \{F_1\} \cup \{0\} = \{F_1, 0\}

Failed to parse (Cannot write to or create math temp directory): 1' \equiv \{F_1\} \cup \{1\} = \{F_1, 1\}

Failed to parse (Cannot write to or create math temp directory): 2' \equiv \{F_1\} \cup \{2\} = \{F_1, 2\}

...
Failed to parse (Cannot write to or create math temp directory): succ'(\{F_1, x\}) \equiv \{F_1, succ(x)\}

Note that we have also defined the successor function, "succ'", with a prime attached to distinguish it from the "succ" function which operates on the natural numbers.

In the remainder of this page, we will use Failed to parse (Cannot write to or create math temp directory): \mathbb{N}

to refer to this set:

Failed to parse (Cannot write to or create math temp directory): \mathbb{N} \equiv \{0', 1', 2', ... \}

We will refer to members of this set as "nonnegative integers".

We can now define the negative integers as:

Failed to parse (Cannot write to or create math temp directory): -1' \equiv \{F_2\} \cup \{1\} = \{F_2, -1\}

Failed to parse (Cannot write to or create math temp directory): -2' \equiv \{F_2\} \cup \{2\} = \{F_2, -2\}

Failed to parse (Cannot write to or create math temp directory): -3' \equiv \{F_2\} \cup \{3\} = \{F_2, -3\}

...
Failed to parse (Cannot write to or create math temp directory): pred'(\{F_2, x\}) \equiv \{F_2, succ(x)\}

The entire set of integers, positive, negative, and zero, will be referred to as I.

We'll need negation later so we define it now:

Failed to parse (Cannot write to or create math temp directory): -(\{F_1,n\}) \equiv \begin{cases} \{F_1,n\}, \mbox{if } n = 0 \\ \{F_2,n\}, \mbox{if } n \neq 0 \end{cases}

Failed to parse (Cannot write to or create math temp directory): -(\{F_2,n\})\, \equiv \{F_1,n\}

and we define > and <, with respect to zero only, as:

Failed to parse (Cannot write to or create math temp directory): x > 0 \equiv x \in (\mathbb{N} - {0})

Failed to parse (Cannot write to or create math temp directory): x < 0 \equiv x \in (\mathbb{I} - \mathbb{N})

For negative integers -- elements of I - N -- we define the succ' function implicitly, by the relation:

Failed to parse (Cannot write to or create math temp directory): succ'(x) = y \equiv x = pred'(y)

along with the special case

Failed to parse (Cannot write to or create math temp directory): succ'(-1') \equiv 0'

and finally we define pred' for values in Failed to parse (Cannot write to or create math temp directory): \mathbb{N}

Failed to parse (Cannot write to or create math temp directory): pred'(\{F_1,x\}) \equiv \begin{cases} \{F_2,1\}, & \mbox{if } x = 0 \\ \{F_1,pred(x)\}, & \mbox{if } x \neq 0 \end{cases}

We can now define the nth successor to a number inductively, as

Failed to parse (Cannot write to or create math temp directory): succ'(x,n) \equiv \begin{cases} x, & \mbox{if } n = 0 \\ succ'(succ'(x),pred'(n)), & \mbox{if }n > 0 \\ succ'(pred'(x),succ'(n)), & \mbox{if }n < 0 \\ \end{cases}

With these definitions in hand, we can define a general "Failed to parse (Cannot write to or create math temp directory): \leq " as

Failed to parse (Cannot write to or create math temp directory): x \leq y \equiv \ \exists n \in \mathbb{N} \left ( y = succ'(x, n) \right )

As with the natural numbers we again can define addition and multiplication in the obvious way.

Failed to parse (Cannot write to or create math temp directory): x + y \equiv succ'(x, y)

Failed to parse (Cannot write to or create math temp directory): x \cdot y \equiv \begin{cases} 0, & \mbox{if } y = 0 \\ x + (x \cdot pred'(y)), & \mbox{if } y > 0 \\ - (x + (x \cdot pred'(-y))), & \mbox{if } y < 0 \end{cases}

This completes the basic model: We have comparisons, addition, and multiplication. The natural numbers, N, are contained within our new model, and comparison in the integers is clearly an extension of comparison in the natural numbers. It's also not hard to show that addition and multiplication are also extensions of the same operations on the natural numbers.

We could now go on to prove the axioms which define the integers as theorems within our model, including particularly the fact that each integer has a unique additive inverse, thus showing that I really is a model of the integers.