nLab natural number

Contents

Contents

Idea

A natural number is traditionally one of the numbers 11, 22, 33, and so on. It is now common in many fields of mathematics to include 00 as a natural number as well. One advantage of doing so is that a natural number can then be identified with the cardinality of a finite set, as well as a finite ordinal number. One can distinguish these as the nonnegative integers (with 00) and the positive integers (without 00), at least until somebody uses ‘positive’ in the semidefinite sense. To a set theorist, a natural number is essentially the same as an integer, so they often use the shorter word; one can also clarify with unsigned integer (but this doesn't help with 00). In school mathematics, natural numbers with 00 are called whole numbers.

The set of natural numbers is often written NN, N\mathbf{N}, \mathbb{N}, ω\omega, or 0\aleph_0. The last two notations refer to this set's structure as an ordinal number or cardinal number respectively, and they often (usually for \aleph) have a subscript 00 allowing them to be generalised. In the foundations of mathematics, the axiom of infinity states that this actually forms a set (rather than a proper class). At a foundational level, it's completely irrelevant whether 00 counts as a natural number or not; as sets (and even as natural numbers objects), the two options are equivalent, so we are really talking about the choice of additive semigroup structure (or inclusion map into the set of integers, etc).

By default, our natural numbers always include 00.

Operations and relations

We define the standard arithmetic and metric operations and order relations of the natural numbers in dependent type theory using induction on the natural numbers.

 Addition

Addition is inductively defined by double induction on the natural numbers

m:,n:m+n:m:\mathbb{N}, n:\mathbb{N} \vdash m + n:\mathbb{N}
β + 0,0:0+0= 0\vdash \beta_+^{0, 0}:0 + 0 =_\mathbb{N} 0
n:β + 0,s(n):0+s(n)= s(n)n:\mathbb{N} \vdash \beta_+^{0, s}(n):0 + s(n) =_\mathbb{N} s(n)
n:β + s,0(n):s(n)+0= s(n)n:\mathbb{N} \vdash \beta_+^{s, 0}(n):s(n) + 0 =_\mathbb{N} s(n)
m:,n:β + s,s(m,n):s(m)+s(n)= s(s(m+n))m:\mathbb{N}, n:\mathbb{N} \vdash \beta_+^{s, s}(m, n):s(m) + s(n) =_\mathbb{N} s(s(m + n))

 Minimum function

The minimum function is inductively defined by double induction on the natural numbers

m:,n:min(m,n):m:\mathbb{N}, n:\mathbb{N} \vdash \min(m, n):\mathbb{N}
β min 0,0:min(0,0)= 0\vdash \beta_\min^{0, 0}:\min(0, 0) =_\mathbb{N} 0
n:β min 0,s(n):min(0,s(n))= 0n:\mathbb{N} \vdash \beta_\min^{0, s}(n):\min(0, s(n)) =_\mathbb{N} 0
n:β min s,0(n):min(s(n),0)= 0n:\mathbb{N} \vdash \beta_\min^{s, 0}(n):\min(s(n), 0) =_\mathbb{N} 0
m:,n:β min s,s(m,n):min(s(m),s(n))= s(min(m,n))m:\mathbb{N}, n:\mathbb{N} \vdash \beta_\min^{s, s}(m, n):\min(s(m), s(n)) =_\mathbb{N} s(\min(m, n))

Maximum function

The maximum function is inductively defined by double induction on the natural numbers

m:,n:max(m,n):m:\mathbb{N}, n:\mathbb{N} \vdash \max(m, n):\mathbb{N}
β max 0,0:max(0,0)= 0\vdash \beta_\max^{0, 0}:\max(0, 0) =_\mathbb{N} 0
n:β max 0,s(n):max(0,s(n))= s(n)n:\mathbb{N} \vdash \beta_\max^{0, s}(n):\max(0, s(n)) =_\mathbb{N} s(n)
n:β max s,0(n):max(s(n),0)= s(n)n:\mathbb{N} \vdash \beta_\max^{s, 0}(n):\max(s(n), 0) =_\mathbb{N} s(n)
m:,n:β max s,s(m,n):max(s(m),s(n))= s(max(m,n))m:\mathbb{N}, n:\mathbb{N} \vdash \beta_\max^{s, s}(m, n):\max(s(m), s(n)) =_\mathbb{N} s(\max(m, n))

 Distance function

The distance function is inductively defined by double induction on the natural numbers

m:,n:ρ(m,n):m:\mathbb{N}, n:\mathbb{N} \vdash \rho(m, n):\mathbb{N}
β ρ 0,0:ρ(0,0)= 0\vdash \beta_\rho^{0, 0}:\rho(0, 0) =_\mathbb{N} 0
n:β ρ 0,s(n):ρ(0,s(n))= s(n)n:\mathbb{N} \vdash \beta_\rho^{0, s}(n):\rho(0, s(n)) =_\mathbb{N} s(n)
n:β ρ s,0(n):ρ(s(n),0)= s(n)n:\mathbb{N} \vdash \beta_\rho^{s, 0}(n):\rho(s(n), 0) =_\mathbb{N} s(n)
m:,n:β ρ s,s(m,n):ρ(s(n),s(n))= ρ(n,n)m:\mathbb{N}, n:\mathbb{N} \vdash \beta_\rho^{s, s}(m, n):\rho(s(n), s(n)) =_\mathbb{N} \rho(n, n)

Absolute value

The absolute value is defined as the distance of a natural number from zero.

n:|n|:n:\mathbb{N} \vdash \vert n \vert:\mathbb{N}
n:δ ||(n):|n|= ρ(n,0)n:\mathbb{N} \vdash \delta_{\vert-\vert}(n):\vert n \vert =_\mathbb{N} \rho(n, 0)

Less than relation

The less than relation is inductively defined by double induction on the natural numbers

m:,n:m<ntypem:\mathbb{N}, n:\mathbb{N} \vdash m \lt n \; \mathrm{type}
β < 0,0:0<0𝟘\vdash \beta_\lt^{0, 0}:0 \lt 0 \simeq \mathbb{0}
n:β < 0,s(n):0<s(n)𝟙n:\mathbb{N} \vdash \beta_\lt^{0, s}(n):0 \lt s(n) \simeq \mathbb{1}
n:β < s,0(n):s(n)<0𝟘n:\mathbb{N} \vdash \beta_\lt^{s, 0}(n):s(n) \lt 0 \simeq \mathbb{0}
m:,n:β < s,s(n):s(m)<s(n)m<nm:\mathbb{N}, n:\mathbb{N} \vdash \beta_\lt^{s, s}(n):s(m) \lt s(n) \simeq m \lt n

Less than or equal to relation

The less than or equal to relation is inductively defined by double induction on the natural numbers

m:,n:mntypem:\mathbb{N}, n:\mathbb{N} \vdash m \leq n \; \mathrm{type}
β 0,0:00𝟙\vdash \beta_\leq^{0, 0}:0 \leq 0 \simeq \mathbb{1}
n:β 0,s(n):0s(n)𝟙n:\mathbb{N} \vdash \beta_\leq^{0, s}(n):0 \leq s(n) \simeq \mathbb{1}
n:β s,0(n):s(n)0𝟘n:\mathbb{N} \vdash \beta_\leq^{s, 0}(n):s(n) \leq 0 \simeq \mathbb{0}
m:,n:β s,s(n):s(m)s(n)mnm:\mathbb{N}, n:\mathbb{N} \vdash \beta_\leq^{s, s}(n):s(m) \leq s(n) \simeq m \leq n

Apart from relation

The apart from relation is inductively defined by double induction on the natural numbers

m:,n:m#ntypem:\mathbb{N}, n:\mathbb{N} \vdash m \# n \; \mathrm{type}
β # 0,0:0#0𝟘\vdash \beta_\#^{0, 0}:0 \# 0 \simeq \mathbb{0}
n:β # 0,s(n):0#s(n)𝟙n:\mathbb{N} \vdash \beta_\#^{0, s}(n):0 \# s(n) \simeq \mathbb{1}
n:β # s,0(n):s(n)#0𝟙n:\mathbb{N} \vdash \beta_\#^{s, 0}(n):s(n) \# 0 \simeq \mathbb{1}
m:,n:β # s,s(n):s(m)#s(n)m#nm:\mathbb{N}, n:\mathbb{N} \vdash \beta_\#^{s, s}(n):s(m) \# s(n) \simeq m \# n

Observational equality relation

The observational equality relation is inductively defined by double induction on the natural numbers

m:,n:mntypem:\mathbb{N}, n:\mathbb{N} \vdash m \doteq n \; \mathrm{type}
β 0,0:00𝟙\vdash \beta_\doteq^{0, 0}:0 \doteq 0 \simeq \mathbb{1}
n:β 0,s(n):0s(n)𝟘n:\mathbb{N} \vdash \beta_\doteq^{0, s}(n):0 \doteq s(n) \simeq \mathbb{0}
n:β s,0(n):s(n)0𝟘n:\mathbb{N} \vdash \beta_\doteq^{s, 0}(n):s(n) \doteq 0 \simeq \mathbb{0}
m:,n:β s,s(n):s(m)s(n)mnm:\mathbb{N}, n:\mathbb{N} \vdash \beta_\doteq^{s, s}(n):s(m) \doteq s(n) \simeq m \doteq n

Greater than relation

The greater than relation is inductively defined by double induction on the natural numbers

m:,n:m>ntypem:\mathbb{N}, n:\mathbb{N} \vdash m \gt n \; \mathrm{type}
β > 0,0:0>0𝟘\vdash \beta_\gt^{0, 0}:0 \gt 0 \simeq \mathbb{0}
n:β > 0,s(n):0>s(n)𝟘n:\mathbb{N} \vdash \beta_\gt^{0, s}(n):0 \gt s(n) \simeq \mathbb{0}
n:β > s,0(n):s(n)>0𝟙n:\mathbb{N} \vdash \beta_\gt^{s, 0}(n):s(n) \gt 0 \simeq \mathbb{1}
m:,n:β > s,s(n):s(m)>s(n)m>nm:\mathbb{N}, n:\mathbb{N} \vdash \beta_\gt^{s, s}(n):s(m) \gt s(n) \simeq m \gt n

Greater than or equal to relation

The greater than or equal to relation is inductively defined by double induction on the natural numbers

m:,n:mntypem:\mathbb{N}, n:\mathbb{N} \vdash m \geq n \; \mathrm{type}
β 0,0:00𝟙\vdash \beta_\geq^{0, 0}:0 \geq 0 \simeq \mathbb{1}
n:β 0,s(n):0s(n)𝟘n:\mathbb{N} \vdash \beta_\geq^{0, s}(n):0 \geq s(n) \simeq \mathbb{0}
n:β s,0(n):s(n)0𝟙n:\mathbb{N} \vdash \beta_\geq^{s, 0}(n):s(n) \geq 0 \simeq \mathbb{1}
m:,n:β s,s(n):s(m)s(n)mnm:\mathbb{N}, n:\mathbb{N} \vdash \beta_\geq^{s, s}(n):s(m) \geq s(n) \simeq m \geq n

Multiplication

Multiplication is inductively defined by induction on the natural numbers

m:,n:m+n:m:\mathbb{N}, n:\mathbb{N} \vdash m + n:\mathbb{N}
n:β 0(n):0n= 0n:\mathbb{N} \vdash \beta_\cdot^{0}(n):0 \cdot n =_\mathbb{N} 0
m:,n:β s(m,n):s(m)n= mn+nm:\mathbb{N}, n:\mathbb{N} \vdash \beta_\cdot^{s}(m, n):s(m) \cdot n =_\mathbb{N} m \cdot n + n

Exponentiation

Exponentiation is inductively defined by induction on the natural numbers

m:,n:n m:m:\mathbb{N}, n:\mathbb{N} \vdash n^m:\mathbb{N}
n:β 0(n):n 0= 1n:\mathbb{N} \vdash \beta_\cdot^{0}(n):n^0 =_\mathbb{N} 1
m:,n:β () () s(m,n):n s(m)= n mnm:\mathbb{N}, n:\mathbb{N} \vdash \beta_{(-)^{(-)}}^{s}(m, n):n^{s(m)} =_\mathbb{N} n^m \cdot n

Division and remainder

Given a natural number nn, we define the division function m÷n:× +m \div n: \mathbb{N} \times \mathbb{N}_{+} \to \mathbb{N} such that

  • for all m:m:\mathbb{N} and n: +n:\mathbb{N}_{+}, if m<nm \lt n then m÷n=0m \div n = 0
  • for all m:m:\mathbb{N} and n: +n:\mathbb{N}_{+}, (m+n)÷n=1+m÷n)(m + n) \div n = 1 + m \div n)

and the remainder function

m%nm(m÷n)nm\ \%\ n \coloneqq m - (m \div n) \cdot n

Natural numbers objects

N\mathbf{N} is a natural numbers object in Set; indeed, it is the original example. This consists of an initial element 00 (or 11 if 00 is not used) and a successor operation nn+1n \mapsto n + 1 (or simply nn +n \mapsto n^+; in computer science, one often writes n+n+) such that, for a set XX, an element a:Xa: X, and a function s:XXs: X \to X, there exists a unique function f:NXf: \mathbf{N} \to X such that f 0=af_0 = a and f n+1=s(f n)f_{n+1} = s(f_n). This function ff is said to be constructed by primitive recursion. (Fancier forms of recursion are also possible.)

The basic idea is that we define the values of ff one by one, starting with f 0=af_0 = a, then f 1=s(a)f_1 = s(a), f 2=s(s(a))f_2 = s(s(a)), and so on. These are all both possible and necessary individually, but something must be put in the foundations to ensure that this can go on uniquely forever.

Properties

Minima of subsets of natural numbers

In classical mathematics, any inhabited subset of the natural numbers possesses a minimal element. In constructive mathematics, one cannot show this:

Proposition

(a Brouwerian counterexample)

If every inhabited subset of the natural numbers possesses a minimal element, then the law of excluded middle holds.

Proof

Let φ\varphi be an arbitrary arithmetical formula. Then the subset

U:={n|n=1φ} U := \{ n \in \mathbb{N} \,|\, n = 1 \vee \varphi \} \subseteq \mathbb{N}

is inhabited. By assumption, it possesses a minimal element n 0n_0. By discreteness of the natural numbers, either n 0=0n_0 = 0 or n 0>0n_0 \gt 0. In the first case, φ\varphi holds. In the second case, ¬φ\neg\varphi holds.

In this sense, the natural numbers are not complete, and it’s fruitful to study their completion: For instance, the global sections of the completed natural numbers object in the sheaf topos on a topological space XX are in one-to-one correspondence with upper semicontinuous functions XX \to \mathbb{N} (details at one-sided real number).

We can salvage the minimum principle in two ways:

Proposition

Any detachable inhabited subset of the natural numbers possesses a minimal element.

Proposition

Any inhabited subset of the natural numbers does not not possess a minimal element.

For instance, any finitely generated vector space over a residue field does not not possess a finite basis (pick a minimal generating set, guaranteed to not not exist). Interpreting this in the internal language of the sheaf topos of a reduced scheme XX, one obtains the well-known fact that any 𝒪 X\mathcal{O}_X-module locally of finite type over XX is locally free on a dense open subset.

Decreasing sequences of natural numbers

Classically, any weakly decreasing sequence of natural numbers (a n) n(a_n)_n is eventually constant, i.e. admits an index NN such that a N=a N+1=a N+2=a_N = a_{N+1} = a_{N+2} = \cdots. Constructively, one can only prove for each MM that there exists an index NN such that a N=a N+1==a N+Ma_N = a_{N+1} = \cdots = a_{N+M}. (One may prove this by induction on a 0a_0; indeed, you can always find NN so that Na 0MN \leq a_0 M.) The classical principle is equivalent to the limited principle of omniscience for \mathbb{N} (which follows already when a 0=1a_0 = 1).

On the other hand, there can be no strictly decreasing sequence of natural numbers. This is constuctively valid (proved by contradiction and induction on a 0a_0).

This is relevant to constructive algebra?, as this shows that formulating chain conditions needs some care. (It is easier to say ‘weakly’ than ‘strictly’ in the hypothesis, but then it's unclear how to state the conclusion.)

Examples

References

Origin of the Dedekind-Peano axioms for the natural numbers:

Review:

Broader historical review:

Last revised on December 16, 2023 at 10:11:57. See the history of this page for a list of all contributions to it.