形式系统

”将哥德尔第二不完全性定理表述为：“如果这样的形式系统是一致的，那么其一致性在本系统中不可证。

哥德尔原本想要证明皮亚诺算术的一致性，当他在工作进行中遇到困难进而猜测一阶皮亚诺算术形式系统有可能存在形式不可证命题并试图证明这一猜测时，他理所当然地必须预设一阶皮亚诺算术形式系统是一致的，因为经典数理逻辑的爆发性，若无此预设则任何命题都形式可证。

哥德尔用于形式化皮亚诺算术的基础逻辑是经典数理逻辑一阶谓词演算，因为经典数理逻辑的爆发性，所以哥德尔在前提条件中必须预设一阶皮亚诺算术形式系统是一致的。

迈耶用于形式化皮亚诺算术的基础逻辑是相关逻辑一阶谓词演算，得益于相关逻辑的准协调性，迈耶在前提条件中无须预设一阶相关皮亚诺算术形式系统是一致的。

“设Z是我们对Peano公理添加了用递归（在一个变量上）定义的模式和限制函数演算的逻辑规则而获得的形式系统。