(Redirected from Sum)

An Arithmetic Addition Operation is an binary arithmetic operation that continues the count of each input.

## References

### 2009

• 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 $n_2$ and $n_3$. The sum of a number $n$ and zero is $n$. (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 "$n_1+S(n_2) = S(n_1+n_2)$".