1 Examples of proof by induction

1.1 The simplest case

Consider the following definition:

f(n) ≐ n = 0\{ \begin{matrix}1 \\ 3 − f(n − 1) \end{matrix}

The function has one variable n ^{·} and that variable is suited to induction in its simplest form because n ^{·} is compared to zero and, if non-zero, f ^{∘} is applied recursively to n − 1 ^{·}.

Mac lemma A : n ∈ N → f(n) ∈ Z

Mac proof of A:

L01 : Definition ⊳  f(n) ≡ if(n = 0, 1, 3 − f(n − 1))  ;
L02 : Block ⊳  Begin  ;
L03 : Hypothesis ⊳  n ∈ N  ;
L04 : Hypothesis ⊳  (n = 0) ∈ T  ;
L05 : IfT ⊳ L4 ⊳  if(n = 0, 1, 3 − f(n − 1)) ≡ 1  ;
L06 : Transitivity ⊳ L1 ⊳ L5 ⊳  f(n) ≡ 1  ;
L07 : TypeNumeralInZ ⊳  1 ∈ Z  ;
L08 : Reverse’ ⊳ L6 ⊳ L7 ⊳  f(n) ∈ Z  ;
L09 : Block ⊳  End  ;
L10 : Block ⊳  Begin  ;
L11 : Hypothesis ⊳  n ∈ N  ;
L12 : Hypothesis ⊳  (n = 0) ∈ F  ;
L13 : Hypothesis ⊳  f(n − 1) ∈ Z  ;
L14 : IfF ⊳ L12 ⊳  if(n = 0, 1, 3 − f(n − 1)) ≡ 3 − f(n − 1) ;
L15 : Transitivity ⊳ L1 ⊳ L14 ⊳  f(n) ≡ 3 − f(n − 1)  ;
L16 : TypeNumeralInZ ⊳  3 ∈ Z  ;
L17 : TypeZ-Z ⊳ L16 ⊳ L13 ⊳  3 − f(n − 1) ∈ Z  ;
L18 : Reverse’ ⊳ L15 ⊳ L17 ⊳  f(n) ∈ Z  ;
L19 : Block ⊳  End  ;
L20 : Induction ⊳ L08 ⊳ L18 ⊳ n ∈ Z → f(n) ∈ Z

In the proof above, note the following:

• It is very often convenient to list definitions at the beginning of the proof. In the present proof, there is one definition of interest, and that definition is stated in Line 1.

• Line 2, 3, 4, 9, 10, 11, 12, 13, and 19 plus the conclusion of Line 8 and 18 can be written down almost automatically once it is decided to prove Line 20 by induction.

A ^{·} rule A

• Line 5 and 6 form an “IfT Transitivity” ideom which simplifies the definition in the given context. Similarly, Line 14 and 15 form an IfF Transitivity ideom.

1.2 The fixed y case

Consider the following definition:

f(x, y) ≐ x = 0\{ \begin{matrix}y \\ f(x − 1, y) + 1 \end{matrix}

The function has two variables, x ^{·} and y ^{·}. x ^{·} is suited to induction because x ^{·} is compared to zero and, if non-zero, f ^{∘} is applied recursively to x−1 ^{·}. y ^{·} is suited for fixation in an outer block because f ^{∘} is applied recursively to an unmodified y ^{·}.

Mac lemma B : y ∈ N → x ∈ N → f(x, y) ∈ N

Mac proof of B:

L01 : Definition ⊳  f(x, y) ≡ if(x = 0, y, f(x − 1, y) + 1)  ;
L02 : Block ⊳  Begin  ;
L03 : Hypothesis ⊳  y ∈ N  ;
L04 : Block ⊳  Begin  ;
L05 : Hypothesis ⊳  x ∈ N  ;
L06 : Hypothesis ⊳  (x = 0) ∈ T  ;
L07 : IfT ⊳ L6 ⊳  if(x = 0, y, f(x − 1, y) + 1) ≡ y  ;
L08 : Transitivity ⊳ L1 ⊳ L7 ⊳  f(x, y) ≡ y  ;
L09 : Reverse’ ⊳ L8 ⊳ L3 ⊳  f(x, y) ∈ N  ;
L10 : Block ⊳  End  ;
L11 : Block ⊳  Begin  ;
L12 : Hypothesis ⊳  x ∈ N  ;
L13 : Hypothesis ⊳  (x = 0) ∈ F  ;
L14 : Hypothesis ⊳  f(x − 1, y) ∈ N  ;
L15 : IfF ⊳ L13 ⊳  if(x = 0, y, f(x − 1, y) + 1) ≡ f(x − 1, y) + 1 ;
L16 : Transitivity ⊳ L1 ⊳ L15 ⊳  f(x, y) ≡ f(x − 1, y) + 1  ;
L17 : TypeNumeralInZ ⊳  1 ∈ N  ;
L18 : TypeN+N ⊳ L14 ⊳ L17 ⊳  f(x − 1, y) + 1 ∈ N  ;
L19 : Reverse’ ⊳ L16 ⊳ L18 ⊳  f(x, y) ∈ N  ;
L20 : Block ⊳  End  ;
L21 : Induction ⊳ L09 ⊳ L19 ⊳  x ∈ N → f(x, y) ∈ N  ;
L22 : Block ⊳  End

B ^{·} rule B

1.3 The variable y case

Consider the following definition:

f(x, y) ≐ x = 0\{ \begin{matrix}y \\ f(x − 1, y + 1) \end{matrix}

The function has two variables, x ^{·} and y ^{·}. x ^{·} is suited to induction because x ^{·} is compared to zero and, if non-zero, f ^{∘} is recursively applied to x − 1 ^{·}. y ^{·} is unsuited for fixation in an outer block y ^{·} changes during the computation of f(x, y) ^{·}.

Mac lemma C : x ∈ N → ∀y∈N: f(x, y) ∈ N

Mac proof of C:

L01 : Definition ⊳  f(x, y) ≡ if(x = 0, y, f(x − 1, y + 1))  ;
L02 : SetN ⊳  N ∈ Set  ;
L03 : Block ⊳  Begin  ;
L04 : Hypothesis ⊳  x ∈ N  ;
L05 : Hypothesis ⊳  (x = 0) ∈ T  ;
L06 : IfT ⊳ L5 ⊳  if(x = 0, y, f(x − 1, y + 1)) ≡ y  ;
L07 : Transitivity ⊳ L1 ⊳ L6 ⊳  f(x, y) ≡ y  ;
L08 : Block ⊳  Begin  ;
L09 : Hypothesis ⊳  y ∈ N  ;
L10 : Reverse’ ⊳ L7 ⊳ L9 ⊳  f(x, y) ∈ N  ;
L11 : Block ⊳  End  ;
L12 : Gen ⊳ L2 ⊳ L10 ⊳  ∀y∈N: f(x, y) ∈ N  ;
L13 : Block ⊳  End  ;
L14 : Block ⊳  Begin  ;
L15 : Hypothesis ⊳  x ∈ N  ;
L16 : Hypothesis ⊳  (x = 0) ∈ F  ;
L17 : Hypothesis ⊳  ∀y∈N: f(x − 1, y) ∈ N  ;
L18 : IfF ⊳ L16 ⊳  if(x = 0, y, f(x − 1, y + 1)) ≡ f(x − 1, y + 1) ;
L19 : Transitivity ⊳ L1 ⊳ L18 ⊳  f(x, y) ≡ f(x − 1, y + 1)  ;
L20 : Block ⊳  Begin  ;
L21 : Hypothesis ⊳  y ∈ N  ;
L22 : TypeNumeralInZ ⊳  1 ∈ N  ;
L23 : TypeN+N ⊳ L21 ⊳ L22 ⊳  y + 1 ∈ N  ;
L24 : ElimAll ⊳ L2 ⊳ L17 ⊳ L23 ⊳  f(x − 1, y + 1) ∈ N  ;
L25 : Reverse’ ⊳ L19 ⊳ L24 ⊳  f(x, y) ∈ N  ;
L26 : Block ⊳  End  ;
L27 : Gen ⊳ L2 ⊳ L25 ⊳  ∀y∈N: f(x, y) ∈ N  ;
L28 : Block ⊳  End  ;
L29 : Induction ⊳ L12 ⊳ L27 ⊳  x ∈ N → ∀y∈N: f(x, y) ∈ N

C ^{·} rule C