Interface:Basic arithmetic

From Wikiproofs
Jump to: navigation, search
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):

param (CLASSICAL Interface:Classical_propositional_calculus () () Unable to load parameter CLASSICAL(Interface:Classical_propositional_calculus)[]+: Unable to load module Interface:Classical_propositional_calculus

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

Unknown command

There are two operations, addition and multiplication:

Unknown command

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.

Unknown command

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

Unknown command

Commutative, associative, and distributive[edit]

Both addition and multiplication are commutative and associative:

Unknown command

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

Unknown command

We can distribute multiplication over addition:

Unknown command

Zero[edit]

There is a constant called 0 which serves as an additive identity:

Unknown command

It also is a multiplicative zero:

Unknown command

One[edit]

There is a constant called 1:

Unknown command

It serves as a multiplicative identity:

Unknown command

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

Unknown command

Order[edit]

We define a formula and supply the usual builders (including some convenience builders).

Unknown command

It has the properties of a total order:

Unknown command

A number of other properties follow from those.

Unknown command

Exactly one of a < b, a = b, or a > b hold.

Unknown command

We also provide some rules, for convenience.

Unknown command

Smallest element[edit]

Zero is the smallest natural number.

Unknown command

Addition is consistent with the order[edit]

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

Unknown command

Multiplication is consistent with the order[edit]

Unknown command

Induction[edit]

There are a number of ways to state induction.

This one is via subst:

Unknown command

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.

Unknown command