A.1.6 Natural numbers

The type of natural numbersMathworldPlanetmath is obtained by introducing primitive constants β„•, 0, and π—Œπ—Žπ–Όπ–Ό with the following rules:

  • β€’


  • β€’


  • β€’


Furthermore, we can define functions by primitive recursion. If we have C:ℕ→𝒰k we can introduce a defined constant f:∏(x:β„•)C⁒(x) whenever we have

d :C⁒(0)
e :∏(x:β„•)(C(x)β†’C(π—Œπ—Žπ–Όπ–Ό(x)))

with the defining equations

f(0):≑d  and  f(π—Œπ—Žπ–Όπ–Ό(x)):≑e(x,f(x)).
Title A.1.6 Natural numbers