Arithmetic is the logicians' favourite term for referring to formal logical theories of natural numbers.
Systems of arithmetic often contain a number of formal operations for constructing natural numbers, such as:
Systems of arithmetic usually allow users to quantify over all natural numbers, i.e. to write statements of the form
where is a predicate involving the variable . In most cases the type annotation is elided.
Finally, systems of arithmetic contain certain principles for arithmetic reasoning, for example
These principles are usually expressible in a first-order language, but not always - see below.
There are many kinds of arithmetic:
Notice that all of these theories are based on first-order systems.
It is possible to formulate a second-order arithmetic, in which one can quantify not only over numbers (), but also over sets of numbers ().
However, this ability usually allows one to define the real numbers. Thus, there is a sense in which the term arithmetic is a misnomer, as we are no longer studying arithmetic, but analysis instead.