Arithmetic Addition Operation

AKA: Addition, Add, Addition Operation, Sum, Summation, Summation Function.
Context:
- It is an Associative Function.
- It can be a part of a Algebraic Summation Operation, such as [math]\displaystyle{ \sum_{i \mathop =1}^{100}i. }[/math]
Example(s):
- [math]\displaystyle{ 1 + 4 \equiv 5. }[/math]
- [math]\displaystyle{ +(1,4) \equiv 5. }[/math]
Counter-Example(s):
See: Counting Function.

References

(Wikipedia, 2011) ⇒ http://en.wikipedia.org/wiki/Arithmetic#Addition_.28.2B.29
- Addition is the basic operation of arithmetic. In its simplest form, addition combines two numbers, the addends or terms, into a single number, the sum of the numbers. Adding more than two numbers can be viewed as repeated addition; this procedure is known as summation and includes ways to add infinitely many numbers in a infinite series; repeated addition of the number one is the most basic form of counting. Addition is commutative and associative so the order the terms are added in does not matter. The identity element of addition (the additive identity) is 0, that is, adding zero to any number yields that same number. Also, the inverse element of addition (the additive inverse) is the opposite of any number, that is, adding the opposite of any number to the number itself yields the additive identity, 0.

http://www.isi.edu/~hobbs/bgt-arithmetic.text
- We will define addition recursively in terms of the "successor" relation. The predication "(sum n1 n2 n3)" means that n1 is the sum of [math]\displaystyle{ n_2 }[/math] and [math]\displaystyle{ n_3 }[/math]. The sum of a number [math]\displaystyle{ n }[/math] and zero is [math]\displaystyle{ n }[/math]. (8) (forall (n) (sum n n 0))
- The recursive step is as follows: (9) (forall (n n1 n2 n3 n4) (if (and (successor n3 n2)(sum n4 n1 n2)) (iff (sum n n1 n3)(successor n n4))))
- The more conventional and more succinct way of saying this is "[math]\displaystyle{ n_1+S(n_2) = S(n_1+n_2) }[/math]".