|
|
| Line 1: |
Line 1: |
| − | The [[integer]]s are the ring of non-fractional numbers:
| + | #REDIRECT [[eng:integer]] |
| − | | + | |
| − | :... -3, -2, -1, 0, 1, 2, 3, ...
| + | |
| − | | + | |
| − | These are the [[natural number]]s, 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 number]]s. Then construct two "flag objects", using pieces of that model:
| + | |
| − | | + | |
| − | :<math>F_1 \equiv \{0,2\} = \{\phi,\{\phi,\{\phi\}\}\}</math>
| + | |
| − | | + | |
| − | :<math>F_2 \equiv \{0,3\} = \{\phi,\{\phi,\{\phi\}, \{\phi, \{\phi\}\}\}\}</math>
| + | |
| − | | + | |
| − | Our model of the natural numbers, as laid out on the
| + | |
| − | [[natural number]]s page, consisted of the sets
| + | |
| − | | + | |
| − | :<math>0 \equiv \Phi = \{\}</math>
| + | |
| − | | + | |
| − | :<math>1 \equiv \{0\}</math>
| + | |
| − | | + | |
| − | :<math>2 \equiv \{0,1\}</math>
| + | |
| − | | + | |
| − | :<math>3 \equiv \{0,1,2\}</math>
| + | |
| − | | + | |
| − | : ...
| + | |
| − | | + | |
| − | We can see by inspection that F<sub>1</sub> and F<sub>2</sub> 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:
| + | |
| − | | + | |
| − | :<math>0' \equiv \{F_1\} \cup \{0\} = \{F_1, 0\}</math>
| + | |
| − | | + | |
| − | :<math>1' \equiv \{F_1\} \cup \{1\} = \{F_1, 1\}</math>
| + | |
| − | | + | |
| − | :<math>2' \equiv \{F_1\} \cup \{2\} = \{F_1, 2\}</math>
| + | |
| − | | + | |
| − | : ...
| + | |
| − | | + | |
| − | :<math>succ'(\{F_1, x\}) \equiv \{F_1, succ(x)\}</math>
| + | |
| − | | + | |
| − | 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 <math>\mathbb{N}</math> to refer to this set:
| + | |
| − | | + | |
| − | :<math>\mathbb{N} \equiv \{0', 1', 2', ... \}</math>
| + | |
| − | | + | |
| − | We will refer to members of this set as "nonnegative integers".
| + | |
| − | | + | |
| − | We can now define the ''negative'' integers as:
| + | |
| − | | + | |
| − | :<math>-1' \equiv \{F_2\} \cup \{1\} = \{F_2, -1\}</math>
| + | |
| − | | + | |
| − | :<math>-2' \equiv \{F_2\} \cup \{2\} = \{F_2, -2\}</math>
| + | |
| − | | + | |
| − | :<math>-3' \equiv \{F_2\} \cup \{3\} = \{F_2, -3\}</math>
| + | |
| − | | + | |
| − | : ...
| + | |
| − | | + | |
| − | :<math>pred'(\{F_2, x\}) \equiv \{F_2, succ(x)\}</math>
| + | |
| − | | + | |
| − | 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:
| + | |
| − | | + | |
| − | :<math>-(\{F_1,n\}) \equiv \begin{cases}
| + | |
| − | \{F_1,n\}, \mbox{if } n = 0 \\
| + | |
| − | \{F_2,n\}, \mbox{if } n \neq 0
| + | |
| − | \end{cases}</math>
| + | |
| − | | + | |
| − | :<math>-(\{F_2,n\})\, \equiv \{F_1,n\}</math>
| + | |
| − | | + | |
| − | and we define > and <, with respect to zero ''only'', as:
| + | |
| − | | + | |
| − | :<math>x > 0 \equiv x \in (\mathbb{N} - {0})</math>
| + | |
| − | | + | |
| − | :<math>x < 0 \equiv x \in (\mathbb{I} - \mathbb{N})</math>
| + | |
| − | | + | |
| − | For ''negative'' integers -- elements of '''I''' - '''N''' -- we
| + | |
| − | define the '''succ'''' function implicitly, by the relation:
| + | |
| − | | + | |
| − | :<math>succ'(x) = y \equiv x = pred'(y)</math>
| + | |
| − | | + | |
| − | along with the special case
| + | |
| − | | + | |
| − | :<math>succ'(-1') \equiv 0'</math>
| + | |
| − | | + | |
| − | and finally we define pred' for values in <math>\mathbb{N}</math>:
| + | |
| − | | + | |
| − | :<math>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}</math>
| + | |
| − | | + | |
| − | We can now define the ''n<sup>th</sup>'' successor to a number
| + | |
| − | inductively, as
| + | |
| − | | + | |
| − | :<math>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}</math>
| + | |
| − | | + | |
| − | With these definitions in hand, we can define a general "<math>\leq</math>" as
| + | |
| − | | + | |
| − | :<math>x \leq y \equiv \ \exists n \in \mathbb{N} \left ( y = succ'(x, n) \right )</math>
| + | |
| − | | + | |
| − | As with the [[natural number]]s we again can define addition and multiplication
| + | |
| − | in the obvious way.
| + | |
| − | | + | |
| − | :<math>x + y \equiv succ'(x, y)</math>
| + | |
| − | | + | |
| − | :<math>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}</math>
| + | |
| − | | + | |
| − | 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.
| + | |
