Editing Integer (section)

==Construction==
=== Traditional development ===
In elementary school teaching, integers are often intuitively defined as the union of the (positive) natural numbers, [[zero]], and the negations of the natural numbers. This can be formalized as follows.<ref>{{cite book |last1=Mendelson |first1=Elliott |title=Number systems and the foundations of analysis |date=1985 |publisher=Malabar, Fla. : R.E. Krieger Pub. Co. |isbn=978-0-89874-818-5 |page=153 |url=https://archive.org/details/numbersystemsfou0000mend/page/152/mode/2up}}</ref> First construct the set of natural numbers according to the [[Peano axioms]], call this <math>P</math>. Then construct a set <math>P^-</math> which is [[Disjoint sets|disjoint]] from <math>P</math> and in one-to-one correspondence with <math>P</math> via a function <math>\psi</math>. For example, take <math>P^-</math> to be the [[ordered pair]]s <math>(1,n)</math> with the mapping <math>\psi = n \mapsto (1,n)</math>. Finally let 0 be some object not in <math>P</math> or <math>P^-</math>, for example the ordered pair (0,0). Then the integers are defined to be the union <math>P \cup P^- \cup \{0\}</math>. 

The traditional arithmetic operations can then be defined on the integers in a [[piecewise]] fashion, for each of positive numbers, negative numbers, and zero. For example [[negation]] is defined as follows:

<math display="block">
-x = \begin{cases}
  \psi(x), & \text{if } x \in P \\
  \psi^{-1}(x), & \text{if } x \in P^- \\
  0, & \text{if } x = 0
\end{cases}
</math>

The traditional style of definition leads to many different cases (each arithmetic operation needs to be defined on each combination of types of integer) and makes it tedious to prove that integers obey the various laws of arithmetic.<ref>{{cite book |title=Number Systems and the Foundations of Analysis |series=Dover Books on Mathematics |first=Elliott |last=Mendelson |publisher=Courier Dover Publications |year=2008 |isbn=978-0-486-45792-5 |page=86 |url=https://books.google.com/books?id=3domViIV7HMC&pg=PA86 |access-date=2016-02-15 |archive-url=https://web.archive.org/web/20161208233040/https://books.google.com/books?id=3domViIV7HMC&pg=PA86 |archive-date=2016-12-08|url-status=live}}.</ref> 

=== Equivalence classes of ordered pairs ===
[[File:Relative numbers representation.svg|thumb|alt=Representation of equivalence classes for the numbers −5 to 5
|Red points represent ordered pairs of [[natural number]]s. Linked red points are equivalence classes representing the blue integers at the end of the line.|upright=1.5]]

In modern set-theoretic mathematics, a more abstract construction<ref>Ivorra Castillo: ''Álgebra''</ref><ref>{{Cite book |last1=Kramer |first1=Jürg |title=From Natural Numbers to Quaternions |last2=von Pippich |first2=Anna-Maria |publisher=Springer Cham |year=2017 |isbn=978-3-319-69427-6 |edition=1st |location=Switzerland |pages=78–81 |language=en |doi=10.1007/978-3-319-69429-0}}</ref> allowing one to define arithmetical operations without any case distinction is often used instead.<ref>{{cite book |title=Learning to Teach Number: A Handbook for Students and Teachers in the Primary School |series=The Stanley Thornes Teaching Primary Maths Series |first=Len |last=Frobisher |publisher=Nelson Thornes |year=1999 |isbn=978-0-7487-3515-0 |page=126 |url=https://books.google.com/books?id=KwJQIt4jQHUC&pg=PA126 |access-date=2016-02-15 |archive-url=https://web.archive.org/web/20161208121843/https://books.google.com/books?id=KwJQIt4jQHUC&pg=PA126 |archive-date=2016-12-08 |url-status=live}}.</ref> The integers can thus be formally constructed as the [[equivalence class]]es of [[ordered pair]]s of [[natural number]]s {{math|(''a'',''b'')}}.<ref name="Campbell-1970-p83">{{cite book |author=Campbell, Howard E. |title=The structure of arithmetic |publisher=Appleton-Century-Crofts |year=1970 |isbn=978-0-390-16895-5 |page=[https://archive.org/details/structureofarith00camp/page/83 83] |url-access=registration |url=https://archive.org/details/structureofarith00camp/page/83 }}</ref>

The intuition is that {{math|(''a'',''b'')}} stands for the result of subtracting {{math|''b''}} from {{math|''a''}}.<ref name="Campbell-1970-p83"/> To confirm our expectation that {{nowrap|1 − 2}} and {{nowrap|4 − 5}} denote the same number, we define an [[equivalence relation]] {{math|~}} on these pairs with the following rule:
:<math>(a,b)\sim(c,d) </math>
precisely when
:<math>a+d=b+c </math>.

Addition and multiplication of integers can be defined in terms of the equivalent operations on the natural numbers;<ref name="Campbell-1970-p83"/> by using {{math|[(''a'',''b'')]}} to denote the equivalence class having {{math|(''a'',''b'')}} as a member, one has:
:<math>[(a,b)]+[(c,d)]:=[(a+c,b+d)]</math>.
:<math>[(a,b)]\cdot[(c,d)]:=[(ac+bd,ad+bc)]</math>.

The negation (or additive inverse) of an integer is obtained by reversing the order of the pair:
:<math>-[(a,b)]:=[(b,a)]</math>.

Hence subtraction can be defined as the addition of the additive inverse:
:<math>[(a,b)]-[(c,d)]:=[(a+d,b+c)]</math>.

The standard ordering on the integers is given by:
:<math>[(a,b)]<[(c,d)]</math> [[if and only if]] <math>a+d<b+c</math>.

It is easily verified that these definitions are independent of the choice of representatives of the equivalence classes.

Every equivalence class has a unique member that is of the form {{math|(''n'',0)}} or {{math|(0,''n'')}} (or both at once). The natural number {{math|''n''}} is identified with the class {{math|[(''n'',0)]}} (i.e., the natural numbers are [[embedding|embedded]] into the integers by map sending {{math|''n''}} to {{math|[(''n'',0)]}}), and the class {{math|[(0,''n'')]}} is denoted {{math|−''n''}} (this covers all remaining classes, and gives the class {{math|[(0,0)]}} a second time since −0&nbsp;=&nbsp;0.

Thus, {{math|[(''a'',''b'')]}} is denoted by
:<math>\begin{cases}a-b,&\mbox{if }a\ge b\\-(b-a),&\mbox{if }a<b\end{cases}</math>

If the natural numbers are identified with the corresponding integers (using the embedding mentioned above), this convention creates no ambiguity.

This notation recovers the familiar [[group representation|representation]] of the integers as {{math|{..., −2, −1, 0, 1, 2, ...} }}.

Some examples are:
:<math>\begin{align}0&=[(0,0)]&=[(1,1)]&=\cdots& &=[(k,k)]\\1&=[(1,0)]&=[(2,1)]&=\cdots&&=[(k+1,k)]\\-1&=[(0,1)]&=[(1,2)]&=\cdots&&=[(k,k+1)]\\2&=[(2,0)]&=[(3,1)]&=\cdots&&=[(k+2,k)]\\-2&=[(0,2)]&= [(1,3)]&=\cdots&&=[(k,k+2)]\end{align}</math>

=== Other approaches ===

In theoretical computer science, other approaches for the construction of integers are used by [[Automated theorem proving|automated theorem provers]] and [[Rewriting|term rewrite engines]]. Integers are represented as [[Term algebra|algebraic terms]] built using a few basic operations (e.g.,  '''zero''', '''succ''', '''pred''') and using [[natural number]]s, which are assumed to be already constructed (using the [[Peano axioms|Peano approach]]).

There exist at least ten such constructions of signed integers.<ref>{{cite conference |last=Garavel |first=Hubert |title=On the Most Suitable Axiomatization of Signed Integers |conference=Post-proceedings of the 23rd International Workshop on Algebraic Development Techniques (WADT'2016) |year=2017 |publisher=Springer |series=Lecture Notes in Computer Science |volume=10644 |pages=120–134 |doi=10.1007/978-3-319-72044-9_9 |isbn=978-3-319-72043-2 |url=https://hal.inria.fr/hal-01667321 |access-date=2018-01-25 |archive-url=https://web.archive.org/web/20180126125528/https://hal.inria.fr/hal-01667321 |archive-date=2018-01-26 |url-status=live }}</ref> These constructions differ in several ways: the number of basic operations used for the construction, the number (usually, between 0 and 2), and the types of arguments accepted by these operations; the presence or absence of natural numbers as arguments of some of these operations, and the fact that these operations are free constructors or not, i.e., that the same integer can be represented using only one or many algebraic terms.

The technique for the construction of integers presented in the previous section corresponds to the particular case where there is a single basic operation '''pair'''<math>(x,y)</math> that takes as arguments two natural numbers <math>x</math> and <math>y</math>, and returns an integer (equal to <math>x-y</math>). This operation is not free since the integer 0 can be written '''pair'''(0,0), or '''pair'''(1,1), or '''pair'''(2,2), etc.. This technique of construction is used by the [[proof assistant]] [[Isabelle (proof assistant)|Isabelle]]; however, many other tools use alternative construction techniques, notable those based upon free constructors, which are simpler and can be implemented more efficiently in computers.