Arithmetic and Induction
Now we can talk about equality in our proof system, we can start to talk about useful things like numbers and arithmetic, and make statements like the fact that addition is commutative (i.e., it doesn't matter which way round we add things):
∀x. ∀y. add(x, y) = add(y, x)
However, we cannot yet prove statements like this. To be able to prove such statements, we use a collection of axioms set out by Giuseppe Peano in the 19th century. These axioms specify a way of representing numbers, the laws for addition and multiplication, and the proof principle of induction, which allows us to prove facts about all natural numbers.
The axioms, including induction, are introduced in the following video, and explained below with exercises in the interactive proof editor.
Representing numbers
Numbers are represented in unary notation. We start from 0 and represent larger numbers by “adding one” many times using the function symbol S, standing for “successor”. So 1 is represented as S(0) (“successsor of zero” or “1 + 0”), 2 is represented as S(S(0)), 3 as S(S(S(0))), and so on.
In order to make sure that the function symbols 0 and S act properly, we need two axioms:
zero-ne-succ: “all x. ¬(0 = S(x))”
This axiom states that 0 is never equal to the successor of something. We need this to make sure that our numbers do not “loop round” back to zero at some point.
succ-injective: “all x. all y. S(x) = S(y) → x = y”
This axiom states that if two successors are equal, then their predecessors are equal. This axiom is a bit more difficult to understand than the previous one. One way to understand it is that it says that there is only one way to “get to” a number in one step. So it is another way of saying that our sequence of numbers has no cycles.
Exercise
With these axioms, we can prove that numbers that are written differently are unequal:
Axioms of Addition
Peano's axioms assume a function symbol “add(x,y)” intended to represent “x + y”. The behaviour of addition is specified by two axioms, which are hopefully almost self-explanatory:
add-zero: “all x. add(0,x) = x”
Adding zero to “x” is equal to “x”. In normal symbols, “0 + x = x”.
add-succ: “all x. all y. add(S(x),y) = S(add(x,y))”
Adding the successor of “x” to “y” is equal to the successor of adding “x” to “y”. In normal symbols, “(1 + x) + y = 1 + (x + y)”.
One way to visualise this axioms is as “pushing” the “S” symbol outside the addition. Most proofs proceed by using the equality in the axiom left-to-right, pushing the “add” symbol down into the term, usually in the hope that the add-zero axiom will apply and the addition will disappear altogether.
Exercise
With these axioms, we can prove simple facts like 2 + 2 = 4:
Axioms of Multiplication
Multiplication is specified in a similar way to addition, by saying what it does on 0 and S in its first argument. Multiplication is represented as repeated addition.
mul-zero: “all x. mul(0,x) = 0”
Multiplying 0 by anything is always 0.
mul-succ: “all x. all y. mul(S(x),y) = add(y,mul(x,y))”
In normal symbols, this axiom says: “(1 + x) * y = y + (x * y)”. As with the add-succ axiom above, we can think of it as pushing the “mul” operation through a layer of successor. Repeated use of this axiom should usually lead to the “mul” operation disappearing when the mul-zero axiom is used.
Exercises
With these axioms for multiplication (and the ones for addition), we can prove facts about arithmetic on specific numbers. For example, 2*2=4:
Induction
The final axiom of Peano's is really an axiom schema: a family of axioms, one for each formula.
The induction axiom schema states that if we want to prove a property P(x) for all numbers x, then we can do so by proving P(0) (the base case) and proving that, for all n, P(n) implies P(S(n)) (the step case).
In symbols, we have an axiom of induction for every formula P(-):
P(0) → (∀n. P(n) → P(S(n))) → (∀x. P(x))
In order to make proofs by induction a bit easier (it can be difficult to select exactly the right formula P to prove), induction has been built into the proof system we are using. This is explained in the following video:
Exercises on Induction
Details on how to do the first few of these are in the video above.
Proof commands...
The blue boxes represent parts of the proof that are unfinished. The comments (in green) tells you what the current goal is. Either the goal is unfocused:
{ goal: <some formula> }
or there is a formula is focus:
{ focus: <formula1>; goal: <formula2> }
The commands that you can use differ according to which mode youare in. The commands correspond directly to the proof rules given in the videos.
Unfocused mode
These rules can be used when there is no formula in the focus. These rules either act on the conclusion directly to break it down into simpler sub-goals, or switch to focused mode (the use
command).
introduce H
can be used when the goal is an implication ‘P → Q’. The nameH
is used to give a name to the new assumption P. The proof then continues proving Q with this new assumption. A green comment is inserted to say what the new named assumption is.introduce y
can be used when the goal is a for all quantification ‘∀x. Q’. The namey
is used for the assumption of an arbitrary individual that we have to prove ‘Q’ for. The proof then continues proving ‘Q’. A green comment is inserted to say that the rest of this branch of the proof is under the assumption that there is a named entity.split
can be used when the goal is a conjunction “P ∧ Q”. The proof will split into two sub-proofs, one to prove the first half of the conjunction “P”, and one to prove the other half “Q”.true
can be used when the goal to prove is ‘T’ (true). This will finish this branch of the proof.left
can be used when the goal to prove is a disjunction ‘P ∨ Q’. A new sub goal will be created to prove ‘P’.right
can be used when the goal to prove is a disjunction ‘P ∨ Q’. A new sub goal will be created to prove ‘Q’.not-intro H
can be used when the goal is a negation ‘¬P’. The nameH
is used to give a name to the new assumption P. The proof then continues proving F (i.e. False) with this new assumption. A green comment is inserted to say what the new named assumption is.exists "t"
can be used when the goal is an exists quantification ‘∃x. Q’. The termt
which must be in quotes, is used as the existential witness and is substituted forx
in Q. The proof then continues proving ‘Q[x:=t]’,refl
can be used when the goal is ‘t = t’ for some term ‘t’. Note that the terms on each side of the equality must be exactly the same. If this command is applicable, then this branch of the proof is complete.NEW
induction x
can be used when the variable ‘x’ is in scope. This will start a proof by induction on ‘x’. The proof will split into two branches, one to prove the case when ‘x = 0’, and one to prove the case when ‘x = S(x1)’. In the latter case, you get to assume the induction-hypothesis which states that the property being proved is true for ‘x1’.use H
can be used whenever there is no current focus.H
is the name of some assumption that is available on this branch of the proof. Named assumptions come from the original statement to be proved, and uses ofintroduce H
,cases H1 H2
,not-intro H
, andunpack y H
.
Focused mode
These rules apply when there is a formula in focus. These rules either act upon the formula in focus, or finish the proof when the focused formula is the same as the goal.
done
can be used when the formula in focus is exactly the same as the goal formula. This will finish this branch of the proof.apply
can be used when the formula in focus is an implication ‘P → Q’. A new subgoal to prove ‘P’ is generated, and the focus becomes ‘Q’ to continue the proof.first
can be used when the formula in focus is a conjunctionP ∧ Q
. The focus then becomes ‘P’, the first part of the conjunction, and the proof continues.second
can be used when the formula in focus is a conjunctionP ∧ Q
. The focus then becomes ‘Q’, the second part of the conjunction, and the proof continues.cases H1 H2
can be used then the formula in focus is a disjunction ‘P ∨ Q’. The proof splits into two branches, one for ‘P’ and one for ‘Q’. The two namesH1
andH2
are used to name the new assumption on the two branches. Green comments are inserted to say what the new named assumptions are.false
can be used when the formula in focus is ‘F’ (false). The proof finishes at this point, no matter what the conclusion is.not-elim
can be used when the formula in focus is a negation ‘¬P’. A new subgoal is generated to prove ‘P’ in order to generate a contradiction.inst "t"
can be used when the formula in focus is of the form ‘∀x. P’. The term t (which must be in quotes) is substituted in the place of x in the formula after the quantifier and the substituted formula ‘P[x:=t]’ remains in focus.unpack y H
can be used when the formula in focus is of the form ‘∃x. P’. The existential is “unpacked” into the assumption of an entityy
and its property ‘P[x:=y]’, which is namedH
. Green comments are inserted to say what the assumption ‘H
’ is.rewrite->
can be used when the formula in focus is an equality ‘t1 = t2’. Every occurrence of ‘t1’ in the goal is rewritten to ‘t2’. (The rewrite goes left to right.)rewrite<-
can be used when the formula in focus is an equality ‘t1 = t2’. Every occurrence of ‘t2’ in the goal is rewritten to ‘t1’. (The rewrite goes right to left.)
add-x-zero: x + 0 = x
(config (assumptions-name "Addition axioms") (assumptions (add-zero "all x. add(0,x) = x") (add-succ "all x. all y. add(S(x),y) = S(add(x,y))")) (goal "all x. add(x,0) = x") (solution (Rule(Introduce x)((Rule(Induction x)((Rule(Use add-zero)((Rule(Instantiate(Fun 0()))((Rule Close())))))(Rule(Use add-succ)((Rule(Instantiate(Var x1))((Rule(Instantiate(Fun 0()))((Rule(Rewrite ltr)((Rule(Use induction-hypothesis)((Rule(Rewrite ltr)((Rule Refl())))))))))))))))))))add-x-succ : x + S(y) = S(x + y)
(config (assumptions-name "Addition axioms") (assumptions (add-zero "all x. add(0,x) = x") (add-succ "all x. all y. add(S(x),y) = S(add(x,y))")) (goal "all x. all y. add(x,S(y)) = S(add(x,y))") (solution (Rule(Introduce x)((Rule(Introduce y)((Rule(Induction x)((Rule(Use add-zero)((Rule(Instantiate(Fun S((Var y))))((Rule(Rewrite ltr)((Rule(Use add-zero)((Rule(Instantiate(Var y))((Rule(Rewrite ltr)((Rule Refl())))))))))))))(Rule(Use add-succ)((Rule(Instantiate(Var x1))((Rule(Instantiate(Fun S((Var y))))((Rule(Rewrite ltr)((Rule(Use induction-hypothesis)((Rule(Rewrite ltr)((Rule(Use add-succ)((Rule(Instantiate(Var x1))((Rule(Instantiate(Var y))((Rule(Rewrite ltr)((Rule Refl())))))))))))))))))))))))))))))Addition is associative:
(config (assumptions-name "Addition axioms") (assumptions (add-zero "all x. add(0,x) = x") (add-succ "all x. all y. add(S(x),y) = S(add(x,y))")) (goal "all x. all y. all z. add(x,add(y,z)) = add(add(x,y),z)") (solution (Rule(Introduce x)((Rule(Introduce y)((Rule(Introduce z)((Rule(Induction x)((Rule(Use add-zero)((Rule(Instantiate(Fun add((Var y)(Var z))))((Rule(Rewrite ltr)((Rule(Use add-zero)((Rule(Instantiate(Var y))((Rule(Rewrite ltr)((Rule Refl())))))))))))))(Rule(Use add-succ)((Rule(Instantiate(Var x1))((Rule(Instantiate(Fun add((Var y)(Var z))))((Rule(Rewrite ltr)((Rule(Use add-succ)((Rule(Instantiate(Var x1))((Rule(Instantiate(Var y))((Rule(Rewrite ltr)((Rule(Use add-succ)((Rule(Instantiate(Fun add((Var x1)(Var y))))((Rule(Instantiate(Var z))((Rule(Rewrite ltr)((Rule(Use induction-hypothesis)((Rule(Rewrite ltr)((Rule Refl())))))))))))))))))))))))))))))))))))))))Addition is commutative:
(config (assumptions-name "Addition axioms + add-x-zero + add-x-succ") (assumptions (add-zero "all x. add(0,x) = x") (add-succ "all x. all y. add(S(x),y) = S(add(x,y))") (add-x-zero "all x. add(x,0) = x") (add-x-succ "all x. all y. add(x,S(y)) = S(add(x,y))")) (goal "all x. all y. add(x,y) = add(y,x)") (solution (Rule(Introduce x)((Rule(Introduce y)((Rule(Induction x)((Rule(Use add-zero)((Rule(Instantiate(Var y))((Rule(Rewrite ltr)((Rule(Use add-x-zero)((Rule(Instantiate(Var y))((Rule(Rewrite ltr)((Rule Refl())))))))))))))(Rule(Use add-succ)((Rule(Instantiate(Var x1))((Rule(Instantiate(Var y))((Rule(Rewrite ltr)((Rule(Use add-x-succ)((Rule(Instantiate(Var y))((Rule(Instantiate(Var x1))((Rule(Rewrite ltr)((Rule(Use induction-hypothesis)((Rule(Rewrite ltr)((Rule Refl())))))))))))))))))))))))))))))Every number is a zero or is a successor of some other number.
(config (assumptions-name "0 and S axioms") (assumptions (zero-ne-succ "all x. ¬(0 = S(x))") (succ-injective "all x. all y. S(x) = S(y) -> x = y")) (goal "all x. x = 0 \/ (ex y. x = S(y))") (solution (Rule(Introduce x)((Rule(Induction x)((Rule Left((Rule Refl())))(Rule Right((Rule(Exists(Var x1))((Rule Refl())))))))))))For all numbers x and y, either they are equal, or they are not. If we assume excluded middle, then this fact is immediate from the fact that every proposition is either true or false. If we do not however, we have to construct a proof. The proof proceeds very similarly to how one might construct a computer program to decide whether two numbers are equal: first check if the first number is zero or successor and then check the second; if they are both zero then they are equal, if one is zero and one is a successor then they are not equal, and they are both successors then check the two smaller numbers.
(config (assumptions-name "0 and S axioms") (assumptions (zero-ne-succ "all x. ¬(0 = S(x))") (succ-injective "all x. all y. S(x) = S(y) -> x = y")) (goal "all x. all y. x = y \/ ¬(x = y)") (solution (Rule(Introduce x)((Rule(Induction x)((Rule(Introduce y)((Rule(Induction y)((Rule Left((Rule Refl())))(Rule Right((Rule(Use zero-ne-succ)((Rule(Instantiate(Var y1))((Rule Close())))))))))))(Rule(Introduce y)((Rule(Induction y)((Rule Right((Rule(NotIntro succ-eq-zero)((Rule(Use zero-ne-succ)((Rule(Instantiate(Var x1))((Rule NotElim((Rule(Use succ-eq-zero)((Rule(Rewrite ltr)((Rule Refl())))))))))))))))(Rule(Use induction-hypothesis)((Rule(Instantiate(Var y1))((Rule(Cases x1-eq-y1 x1-ne-y1)((Rule Left((Rule(Use x1-eq-y1)((Rule(Rewrite ltr)((Rule Refl())))))))(Rule Right((Rule(NotIntro Sx1-eq-Sy1)((Rule(Use x1-ne-y1)((Rule NotElim((Rule(Use succ-injective)((Rule(Instantiate(Var x1))((Rule(Instantiate(Var y1))((Rule Implies_elim((Rule(Use Sx1-eq-Sy1)((Rule Close())))(Rule Close())))))))))))))))))))))))))))))))))We can define “less than or equal” for numbers as x <= y is ∃k. add(x,k) = y. The following proof proves that the numbers are totally ordered: for all pairs of numbers x and y, either x <= y or y <= x.
(config (assumptions-name "Addition axioms") (assumptions (add-zero "all x. add(0,x) = x") (add-succ "all x. all y. add(S(x),y) = S(add(x,y))")) (goal "all x. all y. (ex k. add(x,k) = y) \/ (ex k. add(y,k) = x)") (solution (Rule(Introduce x)((Rule(Induction x)((Rule(Introduce y)((Rule Left((Rule(Exists(Var y))((Rule(Use add-zero)((Rule(Instantiate(Var y))((Rule Close())))))))))))(Rule(Introduce y)((Rule(Induction y)((Rule Right((Rule(Exists(Fun S((Var x1))))((Rule(Use add-zero)((Rule(Instantiate(Fun S((Var x1))))((Rule Close())))))))))(Rule(Use induction-hypothesis)((Rule(Instantiate(Var y1))((Rule(Cases x1-le-y1 y1-le-x1)((Rule Left((Rule(Use x1-le-y1)((Rule(ExElim k add-x1-k-y1)((Rule(Exists(Var k))((Rule(Use add-succ)((Rule(Instantiate(Var x1))((Rule(Instantiate(Var k))((Rule(Rewrite ltr)((Rule(Use add-x1-k-y1)((Rule(Rewrite ltr)((Rule Refl())))))))))))))))))))))(Rule Right((Rule(Use y1-le-x1)((Rule(ExElim k add-y1-k-x1)((Rule(Exists(Var k))((Rule(Use add-succ)((Rule(Instantiate(Var y1))((Rule(Instantiate(Var k))((Rule(Rewrite ltr)((Rule(Use add-y1-k-x1)((Rule(Rewrite ltr)((Rule Refl())))))))))))))))))))))))))))))))))))))Multiplication distributes over addition.
The proof of this fact depends on the associativity and commutativity properties of addition that we proved above. There is a tricky bit of rewriting at the end. It is best to work it out on paper first.
(config (assumptions-name "Addition and Multiplication axioms + add-assoc + add-comm") (assumptions (add-zero "all x. add(0,x) = x") (add-succ "all x. all y. add(S(x),y) = S(add(x,y))") (mul-zero "all x. mul(0,x) = 0") (mul-succ "all x. all y. mul(S(x),y) = add(y,mul(x,y))") (add-assoc "all x. all y. all z. add(x,add(y,z)) = add(add(x,y),z)") (add-comm "all x. all y. add(x,y) = add(y,x)")) (goal "all x. all y. all z. mul(x,add(y,z)) = add(mul(x,y),mul(x,z))") (solution (Rule(Introduce x)((Rule(Introduce y)((Rule(Introduce z)((Rule(Induction x)((Rule(Use mul-zero)((Rule(Instantiate(Fun add((Var y)(Var z))))((Rule(Rewrite ltr)((Rule(Use mul-zero)((Rule(Instantiate(Var y))((Rule(Rewrite ltr)((Rule(Use mul-zero)((Rule(Instantiate(Var z))((Rule(Rewrite ltr)((Rule(Use add-zero)((Rule(Instantiate(Fun 0()))((Rule(Rewrite ltr)((Rule Refl())))))))))))))))))))))))))(Rule(Use mul-succ)((Rule(Instantiate(Var x1))((Rule(Instantiate(Fun add((Var y)(Var z))))((Rule(Rewrite ltr)((Rule(Use mul-succ)((Rule(Instantiate(Var x1))((Rule(Instantiate(Var y))((Rule(Rewrite ltr)((Rule(Use mul-succ)((Rule(Instantiate(Var x1))((Rule(Instantiate(Var z))((Rule(Rewrite ltr)((Rule(Use induction-hypothesis)((Rule(Rewrite ltr)((Rule(Use add-assoc)((Rule(Instantiate(Var y))((Rule(Instantiate(Var z))((Rule(Instantiate(Fun add((Fun mul((Var x1)(Var y)))(Fun mul((Var x1)(Var z))))))((Rule(Rewrite rtl)((Rule(Use add-assoc)((Rule(Instantiate(Var z))((Rule(Instantiate(Fun mul((Var x1)(Var y))))((Rule(Instantiate(Fun mul((Var x1)(Var z))))((Rule(Rewrite ltr)((Rule(Use add-comm)((Rule(Instantiate(Var z))((Rule(Instantiate(Fun mul((Var x1)(Var y))))((Rule(Rewrite ltr)((Rule(Use add-assoc)((Rule(Instantiate(Fun mul((Var x1)(Var y))))((Rule(Instantiate(Var z))((Rule(Instantiate(Fun mul((Var x1)(Var z))))((Rule(Rewrite rtl)((Rule(Use add-assoc)((Rule(Instantiate(Var y))((Rule(Instantiate(Fun mul((Var x1)(Var y))))((Rule(Instantiate(Fun add((Var z)(Fun mul((Var x1)(Var z))))))((Rule Close())))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))