关于整数的形式理论NT可以嵌入到Z1中,NT的形式理论： 　　(1) Sx≠0 　　(2) Sx = Sy→x = y 　　(3) x+0 = x 　　(4) x + Sy = S(x+y) 　　(5) x·0 = 0 　　(6) x·Sy = (x·y) + x 　　(7) ( x < 0 ) 　　(8) x < Syx< y ∨ x = y 　　(9) x <y ∨ x = y ∨ y < x 　　这里形式谓词S, < 分别代表后继( 加1 ),小于。二者都可以在Z1中定义Sxx +1,x < yz( z≠∧ x + z = y )。读者可以自行验证，NT的每一条公理在Z1中都是可证的。 　　由于Z1包含了N, 我们有了对Z1的公式，形式规则，包括形成规则、推理规则、形式证明等等进行 Godel 编码的基础设置，这对介绍 Godel 不完全性定理的证明是必须的。