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 () ())
param (FIRSTORDER Interface:First-order_logic_with_quantifiability (CLASSICAL) ())

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

kindbind (object nat)
var (nat a b c d a0 a1 b0 b1)

There are two operations, addition and multiplication:

term (nat (+ nat nat))
term (nat (· nat nat))

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.

stmt (AdditionBuilder () () (((a0 = a1)  (b0 = b1))  ((a0 + b0) = (a1 + b1))))

stmt (AdditionBuilderLL () () ((b0 = b1)  ((a + b0) = (a + b1))))
stmt (AdditionBuilderRR () () ((a0 = a1)  ((a0 + b) = (a1 + b))))

stmt (buildAddition () ((a0 = a1) (b0 = b1)) ((a0 + b0) = (a1 + b1)))

stmt (buildAdditionLL () ((b0 = b1)) ((a + b0) = (a + b1)))
stmt (buildAdditionRR () ((a0 = a1)) ((a0 + b) = (a1 + b)))

stmt (MultiplicationBuilder () () (((a0 = a1)  (b0 = b1))  ((a0 · b0) = (a1 · b1))))

stmt (MultiplicationBuilderLL () () ((b0 = b1)  ((a · b0) = (a · b1))))
stmt (MultiplicationBuilderRR () () ((a0 = a1)  ((a0 · b) = (a1 · b))))

stmt (buildMultiplication () ((a0 = a1) (b0 = b1)) ((a0 · b0) = (a1 · b1)))

stmt (buildMultiplicationLL () ((b0 = b1)) ((a · b0) = (a · b1)))
stmt (buildMultiplicationRR () ((a0 = a1)) ((a0 · b) = (a1 · b)))

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

stmt (AdditionCancellationRight () () (((a + c) = (b + c))  (a = b)))
stmt (cancelAdditionRight () (((a + c) = (b + c))) (a = b))
stmt (AdditionCancellationLeft () () (((c + a) = (c + b))  (a = b)))
stmt (cancelAdditionLeft () (((c + a) = (c + b))) (a = b))

Commutative, associative, and distributive[edit]

Both addition and multiplication are commutative and associative:

stmt (AdditionCommutativity () () ((a + b) = (b + a)))
stmt (AdditionAssociativity () ()
  (((a + b) + c) = (a + (b + c))))

stmt (MultiplicationCommutativity () () 
  ((a · b) = (b · a)))
stmt (MultiplicationAssociativity () ()
  (((a · b) · c) = (a · (b · c))))

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

stmt (Addition4 () () (((a + b) + (c + d)) = ((a + c) + (b + d))))

We can distribute multiplication over addition:

stmt (LeftDistribution () ()
  ((a · (b + c)) = ((a · b) + (a · c))))
stmt (RightDistribution () ()
  (((a + b) · c) = ((a · c) + (b · c))))

Zero[edit]

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

term (nat (0))

stmt (AdditiveIdentityLeft () () (((0) + a) = a))
stmt (AdditiveIdentityRight () () ((a + (0)) = a))

It also is a multiplicative zero:

stmt (MultiplicativeZeroLeft () () (((0) · a) = (0)))
stmt (MultiplicativeZeroRight () () ((a · (0)) = (0)))

One[edit]

There is a constant called 1:

term (nat (1))

It serves as a multiplicative identity:

stmt (MultiplicativeIdentityRight () ()
  ((a · (1)) = a))
stmt (MultiplicativeIdentityLeft () ()
  (((1) · a) = a))

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

stmt (ZeroOne () () ((0)  (1)))

Order[edit]

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

term (formula ( nat nat))

stmt (LessEqualBuilder () () (((a0 = a1)  (b0 = b1))  ((a0  b0)  (a1  b1))))
stmt (LessEqualBuilderLL () () ((b0 = b1)  ((a  b0)  (a  b1))))
stmt (LessEqualBuilderRR () () ((a0 = a1)  ((a0  b)  (a1  b))))

It has the properties of a total order:

stmt (LessEqualTransitivity () () (((a  b)  (b  c))  (a  c)))
stmt (LessEqualAntisymmetry () () (((a  b)  (b  a))  (a = b)))
stmt (LessEqualTotality () () ((a  b)  (b  a)))

A number of other properties follow from those.

stmt (LessEqualReflexivity () () (a  a))

term (formula (< nat nat))
def ((> b a) (a < b))
def (( b a) (a  b))

stmt (LessEqualLessThan () () ((a  b)  ((a < b)  (a = b))))
stmt (LessThanLessEqual () () ((a < b)  ((a  b)  (a  b))))

stmt (LessThanBuilder () () (((a0 = a1)  (b0 = b1))  ((a0 < b0)  (a1 < b1))))
stmt (LessThanBuilderLL () () ((b0 = b1)  ((a < b0)  (a < b1))))
stmt (LessThanBuilderRR () () ((a0 = a1)  ((a0 < b)  (a1 < b))))

stmt (LessEqualLessThanTransitivity () () (((a  b)  (b < c))  (a < c)))
stmt (LessThanTransitivity () () (((a < b)  (b < c))  (a < c)))

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

stmt (LessThanTotality () () (((a < b)  (a = b))  (a > b)))
stmt (LessThanEquality () () ((a < b)  (a  b)))
stmt (LessThanGreaterThan () () ((a < b)  (¬ (a > b))))
stmt (EqualityLessThan () () ((a = b)  (¬ (a < b))))

We also provide some rules, for convenience.

stmt (buildLessThan () ((a0 = a1) (b0 = b1)) ((a0 < b0)  (a1 < b1)))
stmt (buildLessThanLL () ((b0 = b1)) ((a < b0)  (a < b1)))
stmt (buildLessThanRR () ((a0 = a1)) ((a0 < b)  (a1 < b)))

Smallest element[edit]

Zero is the smallest natural number.

stmt (ZeroSmallest () () ((0)  a))

Addition is consistent with the order[edit]

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

stmt (LessEqualAddition () () (((a0  a1)  (b0  b1))  ((a0 + b0)  (a1 + b1))))
stmt (LessEqualAdditionRR () () ((a0  a1)  ((a0 + b)  (a1 + b))))
stmt (LessEqualAdditionLL () () ((b0  b1)  ((a + b0)  (a + b1))))

stmt (LessThanAddition () () (((a0 < a1)  (b0 < b1))  ((a0 + b0) < (a1 + b1))))
stmt (LessThanAdditionRR () () ((a0 < a1)  ((a0 + b) < (a1 + b))))
stmt (LessThanAdditionLL () () ((b0 < b1)  ((a + b0) < (a + b1))))

stmt (LessEqualLessThanAddition () () (((a0  a1)  (b0 < b1))  ((a0 + b0) < (a1 + b1))))

Multiplication is consistent with the order[edit]

stmt (LessEqualMultiplicationRR () () ((a  b)  ((a · c)  (b · c))))

Induction[edit]

There are a number of ways to state induction.

This one is via subst:

var (formula φ)
var (variable k n)

stmt (InductionSubst () () 
  (((subst (0) n φ)  
    ( k ((subst (value k) n φ)  (subst ((value k) + (1)) n φ)))) 
    ( n φ)))

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.

var (formula φ0 φk φSk φa)

stmt (Induction6 ((n a) (φ0 n) (φk n) (φSk n) (φa n) (φ k) (n k))
  ((((value n) = (0))  (φ  φ0))
   (((value n) = (value k))  (φ  φk))
   (((value n) = ((value k) + (1)))  (φ  φSk))
   (((value n) = a)  (φ  φa))
   φ0
   (φk  φSk)
  )
  φa)

Interface module parsed successfully