1 2乗

\(m^n\) は \(m\) の \(n\) 乗（ソースでは m ↑ n・0.book の ↑𝕄）。
↑2 … \(m \in \mathbb{M} \Longrightarrow m ^ 2 = m \cdot m\) \(\blacktriangleleft\) 𝕄0s ，IND𝕄 ，+𝕄 ，*𝕄 ，↑𝕄 ，1. ，2.

2 偶数と奇数

どの自然数も \(2k\) か \(2k+1\) のどちらか一方の形（0.book の Lpar・Lne）。奇数の2乗は奇数なので、\(m^2\) が偶数なら \(m\) は偶数（Lev）。
Lev … \(m , x \in \mathbb{M} , m \cdot m = 2 \cdot x \Longrightarrow \exists k \in \mathbb{M} . m = 2 \cdot k\) \(\blacktriangleleft\) 𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，*𝕄 ，1. ，2.

3 主定理

\(\sqrt{2}\) が分数 \(m/n\)（\(n \neq 0\)）で書けるなら \(m^2 = 2n^2\)。この本は有理数・実数を扱わないので、この言い換えは本の外で行い、本は「そのような自然数 \(m, n\) は無い」ことを示す（√2∄）。
\(m^2 = 2n^2\) なら \(m^2\) は偶数なので \(m = 2k\)、すると \(n^2 = 2k^2\) で \(n = 2j\)、さらに \(k^2 = 2j^2\)。
\(n \neq 0\) なら \(j < n\) で同じ形の解 \((k, j)\) ができる（無限降下）。\(n\) についての強い帰納法（SIND𝕄）で \(n = 0\)。
√2 … \(m , n \in \mathbb{M} , m ^ 2 = 2 \cdot n ^ 2 \Longrightarrow n = 0\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，*𝕄 ，↑𝕄
すなわち \(m^2 = 2n^2\)、\(n \neq 0\) となる自然数 \(m, n\) は無い。
√2∄ … \(\neg \exists m \in \mathbb{M} . \exists n \in \mathbb{M} . n \neq 0 , m ^ 2 = 2 \cdot n ^ 2\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，*𝕄 ，↑𝕄