construction axiom construction axiom
⊤
⇒ 0: nat
⇒ 0+1: nat+1
⇒ 1: nat
⇒ 1+1: nat+1
⇒ 2: nat
0: nat nat+1: nat
Recursive Data Definition
example: nat
can be constructed by starting with 0 and repeatedly adding 1
by the axiom, 0: nat add 1 to each side by arithmetic, 0+1 = 1 ; by the axiom, nat+1: nat add 1 to each side by arithmetic, 1+1 = 2 ; by the axiom, nat+1: nat and so on
1/20
construction axiom construction axiom
0: nat nat+1: nat
?
nat = nat = nat = nat = nat =
0, 1, 2, 3, 4, 5, …
…, -3, -2, -1, 0, 1, 2, 3, … ?
the rationals ?
the reals ?
0, 0.5, 1, 1.5, 2, 2.5, 3, 3.5, … ?
Recursive Data Definition
example: nat
can be constructed by starting with 0 and repeatedly adding 1
2/20
Recursive Data Definition
example: nat
can be constructed by starting with 0 and repeatedly adding 1
construction axiom construction axiom induction axiom
construction axiom induction axiom
construction axiom induction axiom
0: nat
nat+1: nat
0: B ∧ B+1: B ⇒ nat: B
0, nat+1: nat
0, B+1: B ⇒ nat: B
P0 ∧ ∀n: nat· Pn ⇒ P(n+1) ⇐ P0 ∧ ∀n: nat· Pn ⇒ P(n+1) ⇒
∀n: nat· Pn ∀n: nat· Pn
3/20
Recursive Data Definition
nat induction
P0∧∀n:nat·Pn⇒P(n+1) ⇒ ∀n:nat·Pn
P0 ∨ ∃n: nat· ¬Pn ∧ P(n+1) ⇐ ∃n: nat· Pn
∀n: nat· Pn ⇒ P(n+1) ⇒
∃n: nat· ¬Pn ∧ P(n+1) ⇐
∀n: nat· (∀m: nat· m