Def：successor function
自然数の集合を $\mathbb{N}$ とする.後者関数とは,写像\[S : \mathbb{N} \to \mathbb{N}\]であって,任意の $n \in \mathbb{N}$ に対して\[S(n) = n + 1\]を満たす関数である.
ペアノ算術において,後者関数 $S$ は次の性質を持つ：\[\begin{align}&\text{(1) } 0 \in \mathbb{N}, \\&\text{(2) } \forall n \in \mathbb{N}, \; S(n) \in \mathbb{N}, \\&\text{(3) } \forall n \in \mathbb{N}, \; S(n) \neq 0, \\&\text{(4) } \forall m,n \in \mathbb{N}, \; S(m) = S(n) \implies m = n.\end{align}\]
フォン・ノイマンの自然数構成において,後者関数は\[S(n) = n \cup \{n\}\]で定義される.
後者関数 $S(n)$ の操作は「既存の集合 $n$ に,そのもの自身を 1 つ要素として加える」というものである.すなわち,\[S(0) = 0 \cup \{0\} = \varnothing \cup \{\varnothing\} = 1\]\[S(1) = 1 \cup \{1\} = \{\varnothing\} \cup \{\{\varnothing\}\} = 2\]\[S(2) = 2 \cup \{2\} = \{\varnothing, \{\varnothing\}\} \cup \{\{\varnothing, \{\varnothing\}\}\} = 3\]と順に「次の自然数」が構成される.
Lean 4 において,自然数型 Nat は 帰納的型[inductive type] として次のように定義される.
inductive Nat where
| zero : Nat
| succ : Nat → Nat
ここで,zero は $0$ を表す定数コンストラクタ.$\mathsf{succ} : \mathbb{N} \to \mathbb{N}$ は,後者関数[successor function]であり,引数の自然数に $1$ を加えることを表している.
Mathematics is the language with which God has written the universe.