关于整数的形式理论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 不完全性定理的证明是必须的。