超越哥德尔：简洁一致的构造型一阶Peano算术系统，不通过哥德尔的推理产生不可判定命题
摘要：形式系统的第一阶算术能够有效地证明戈德尔不可判定命题的存在，我们认为这种形式系统存在异常的非构造性。 我们认为，在这样的系统中，原始递归谓词的强表示允许异常的非构造性、柏拉图主义的元素进入形式系统中，而这些元素在其所意图形式化的谓词中并没有反映出来。 我们认为，这些系统中异常的柏拉图主义元素的来源是一阶逻辑的非构造性概括规则。 我们认为，在大多数忠实地形式化直觉算术的简单一致系统中，我们不能从哥德尔的推理中推论出形式上不可判定但在每个解释下为真的异常非构造命题的柏拉图主义存在。 我们定义了一个具有建设性的Peano算术形式系统，omega2-PA，其公理与标准Peano算术PA的公理相同，但导致了显著不同的逻辑结果。 因此，我们认为真正数学命题的形式不可判定性是特定的形式化选择所具有的特征，而不是任何自然数算术中内在于柏拉图主义的关系的特征。
作者：Bhupinder Singh Anand
论文ID：math/0201059
分类：General Mathematics
分类简称：math.GM
提交时间：2007-05-23