# Interface:Basic arithmetic

Module usage |
---|

Parameters |

Classical propositional calculus, first-order logic |

Imported by |

None yet. |

Exported by |

Basic arithmetic |

This page covers basic arithmetic, up to the familiar laws of arithmetic: commutative, associative, distributive, etc. At least for now, it stops before continuing into number theory (divisibility, primes, etc).

We build on propositional logic and first-order logic (including equality):

The kind `object`

, defined in first-order logic, represents a natural number:

There are two operations, addition and multiplication:

## Contents

## Builders[edit]

Equals can be substituted for equals, in the context of addition and multiplication. We provide a number of convenience builders in addition to the basic ones.

The converse of some of the builders hold and are known as cancellation laws.

## Commutative, associative, and distributive[edit]

Both addition and multiplication are commutative and associative:

We also provide a convenience theorem which applies commutativity and associativity in a common way:

We can distribute multiplication over addition:

## Zero[edit]

There is a constant called `0`

which serves as an additive identity:

It also is a multiplicative zero:

## One[edit]

There is a constant called `1`

:

It serves as a multiplicative identity:

As with a field, the additive identity does not equal the multiplicative identity.

## Order[edit]

We define a formula `≤`

and supply the usual builders (including some convenience builders).

It has the properties of a total order:

A number of other properties follow from those.

Exactly one of `a < b`

, `a = b`

, or `a > b`

hold.

We also provide some rules, for convenience.

### Smallest element[edit]

Zero is the smallest natural number.

### Addition is consistent with the order[edit]

Assuming one of these implies the others fairly directly, but we supply them all as convenience theorems.

### Multiplication is consistent with the order[edit]

## Induction[edit]

There are a number of ways to state induction.

This one is via `subst`

:

This one has six hypotheses, which despite the large number turns out to be easier to handle than `InductionSubst`

. The first four hypotheses handle the substitution machinery. The last two express the base case and induction step, and because the substitution has already been taken care of, tend to contain more mathematically interesting content and less substitution machinery.