关于整数的形式理论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) ![]() (8) x < Sy ![]() (9) x <y ∨ x = y ∨ y < x 这里形式谓词S, < 分别代表后继( 加1 ),小于。二者都可以在Z1中定义Sx ![]() ![]() ![]() 由于Z1包含了N, 我们有了对Z1的公式,形式规则,包括形成规则、推理规则、形式证明等等进行 Godel 编码的基础设置,这对介绍 Godel 不完全性定理的证明是必须的。 |