articles2/0（集合を使わない算術の土台）で公理として置いたものが、word_basis の自然数（ノイマンの作り方）で成り立つことを示す。後者は \(n + 1\) と書く（articles2/0 は suc を使わない）。
加法・乗法・べきの漸化式（+𝕄・⋅𝕄・↑𝕄）、帰納法（INDC）、順序（≤.・<.）、約数（∣.）、正の自然数（ℕ.'）は、word_basis に同じ式であるので、ここで示すのは次の3つ：ペアノの条件、数字 1〜5、正の自然数 ℕ.'。

1 ペアノの公理

0 は自然数、後者は自然数で 0 でなく、後者が等しければ等しい。
\(0 \in \mathbb{M} , \forall n \in \mathbb{M} . n + 1 \in \mathbb{M} , \forall n \in \mathbb{M} . n + 1 \neq 0 , \forall m \in \mathbb{M} . \forall n \in \mathbb{M} . ( m + 1 = n + 1 \Longrightarrow m = n )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，\(0 \in \mathbb{M}\) ，𝕄1 ，L+1≠0 ，L+1c

2 数字

articles2/0 では \n = (\n-1) + 1（\n.）を公理とした。word_basis では同じ式が定理（1.. 〜 5..）として証明されている。
\(1 = 0 + 1 , 2 = 1 + 1 , 3 = 2 + 1 , 4 = 3 + 1 , 5 = 4 + 1\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，\(0 \in \mathbb{M}\) ，𝕄1

3 正の自然数

articles2/0 では ℕ.'（\(n \in \mathbb{N} \iff n \in \mathbb{M}\) かつ \(n \neq 0\)）を公理とした。word_basis では ℕ を 𝕄 から 1 を除いたものと定め、同じ式を定理（ℕ.'）として示している。
\(\forall n \, ( n \in \mathbb{N} \Longleftrightarrow n \in \mathbb{M} , n \neq 0 )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，\(0 \in \mathbb{M}\) ，𝕄1
articles2/Z で公理とした整数の式が、word_basis の整数で成り立つことを示す。-ℤ・+ℤ・⋅ℤ は word_basis にも同じ式の Prop としてあるので、ここで示すのは ℤ の所属の条件（ℤ.'）だけ。

4 整数の所属

word_basis では ℤ = 𝕄 ∪ (^- ℕ) と集合で定義している。articles2/Z ではこれを所属の条件として公理にした。
\(\forall z \, ( z \in \mathbb{Z} \Longleftrightarrow z \in \mathbb{M} \mathbin{\rm o\!r} \exists n \in \mathbb{N} . z = - n )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ

5 列の存在（型つき）

articles2/0 は、列を原始記号 ap の値として扱い、「1 点だけ値を変えた列が在る（UPD）」「頭に 1 項を足した列が在る（SEQ）」を、どんな対象にも成り立つ公理とした。word_basis の ap は関数（写像）にだけ値が決まるので、成り立つのは関数に限った形で、これを示す。
arith の定理を word_basis で読むときは、列を 𝕄 → A の写像と読み、UPD・SEQ をこの形で使う。
\(f \in ( \mathbb{M} \to A ) , k \in \mathbb{M} , p \in A \Longrightarrow \exists g \in ( \mathbb{M} \to A ) . ( g ( k ) = p , \forall i \in \mathbb{M} . ( i \neq k \Longrightarrow g ( i ) = f ( i ) ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，ap. ，=_. ，UPD
\(f \in ( \mathbb{M} \to A ) , p \in A \Longrightarrow \exists g \in ( \mathbb{M} \to A ) . ( g ( 0 ) = p , \forall i \in \mathbb{M} . g ( ( i + 1 ) ) = f ( i ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，ap. ，=_. ，SEQ

6 列の和（型つき）

articles2/0 は、列の和 f sum n を原始記号とし、漸化式（sum𝕄）を公理とした。word_basis では ∑（AxΣ）で、f を n に制限した写像の和として定義する。
arith の漸化式 (f sum (n + 1)) = (f sum n) + f ap (n) は、n + 1 を変数 k に置いた形で示す（k = n + 1）。
word(ss,s) … \(\sum\)
sum. … \(f \sum n = \sum ( \lceil i \mapsto f ( i ) \rfloor | _ n )\)
\(f \in ( \mathbb{M} \to V ) \Longrightarrow ( f \sum 0 ) = 0\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，AxΣ ，ap. ，=_.
\(f \in ( \mathbb{M} \to V ) , n \in \mathbb{M} , k = n + 1 \Longrightarrow ( f \sum k ) = ( f \sum n ) + f ( n )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，AxΣ ，ap. ，=_.

7 列の積（型つき）

articles2/0 は、列の積 f prod n を原始記号とし、漸化式（prod𝕄）を公理とした。word_basis では ⨉（AxΠ）で、f を n に制限した写像の積として定義する。
arith の漸化式 (f prod (n + 1)) = (f prod n) ⋅ f ap (n) は、n + 1 を変数 k に置いた形で示す（k = n + 1）。
word(ss,s) … \(\prod\)
prod. … \(f \prod n = \mathrm{\Pi} ( \lceil i \mapsto f ( i ) \rfloor | _ n )\)
\(f \in ( \mathbb{M} \to V ) \Longrightarrow ( f \prod 0 ) = 1\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，AxΠ ，ap. ，=_.
\(f \in ( \mathbb{M} \to V ) , n \in \mathbb{M} , k = n + 1 \Longrightarrow ( f \prod k ) = ( f \prod n ) \cdot f ( n )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，AxΠ ，ap. ，=_.