\(n_{1},n_{2}:\mathbb {N}\)を要素とする。要素\(\mathord {\textnormal {\textsf {plus}}}(n_{1},n_{2}):\mathbb {N}\)を構成する。自然数の帰納法を使い、\(\mathord {\textnormal {\textsf {plus}}}(0,n_{2})\equiv n_{2}\)と\(\mathord {\textnormal {\textsf {plus}}}(\mathord {\textnormal {\textsf {succ}}}(n_{1}),n_{2})\equiv \mathord {\textnormal {\textsf {succ}}}(\mathord {\textnormal {\textsf {plus}}}(n_{1},n_{2}))\)と定義する。形式的には\(\mathord {\textnormal {\textsf {plus}}}(n_{1},n_{2})\equiv \mathord {\textnormal {\textsf {ind}}}_{\mathbb {N}}(n_{1},\lambda x.\mathbb {N},n_{2},\lambda (x,y).\mathord {\textnormal {\textsf {succ}}}(y))\)と定義できる。