Arithmetic

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:

• constants
• addition
• multiplication
• exponentiation

Systems of arithmetic usually allow users to quantify over all natural numbers, i.e. to write statements of the form

  \forall x : \mathbb{N}.\ \phi(x)

where \phi(x) is a predicate involving the variable x. In most cases the type annotation is elided.

Finally, systems of arithmetic contain certain principles for arithmetic reasoning, for example

• induction

These principles are usually expressible in a first-order language, but not always - see below.

Examples

There are many kinds of arithmetic:

• Peano arithmetic
• Heyting arithmetic
• Presburger arithmetic

Notice that all of these theories are based on first-order systems.

Second-order arithmetic

It is possible to formulate a second-order arithmetic, in which one can quantify not only over numbers (\forall x : \mathbb{N}), but also over sets of numbers (\forall P : \mathcal{P}(\mathbb{N})).

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.

References

• Second-order arithmetic on Wikipedia.