戈德尔的不完整定理，停止问题和通用图灵机之间是否有任何具体关系？
https://cs.stackexchange.com/questions/419
-
16-10-2019 - |
italiano
english
français
española
中国
日本の
العربية
Deutsch
한국어
Português
Russian题
我一直隐约认为上述问题的答案在以下几行上是肯定的。戈德尔的不完整定理和停止问题的不确定性既是对可决定性的负面结果，又是通过对角线论点（以及1930年代）确定的，因此它们必须以某种方式是两种查看相同问题的方法。我认为图灵使用通用的图灵机表明停止问题是无法解决的。 （也可以看看 这个数学 问题。）
但是，既然这个（教授可计算性的课程），我仔细研究了这些问题，我对发现的东西感到困惑。因此，我希望提供一些帮助，以拉直自己的想法。我意识到，一方面，戈德尔的对角线论点非常微妙：需要大量工作来构建算术陈述，该算法可以解释为对其自身的衍生性说明。另一方面，我发现停止问题的不确定性的证明 这里 非常简单，甚至没有明确提及图灵机，更不用说通用图灵机的存在了。
关于通用图灵机器的一个实用问题是，通用图灵机的字母是否与模拟的图灵机的字母相同，是否有任何重要的问题。我认为这是为了炮制适当的对角线论点（让机器模拟自己）是必要的，但是在我在网络上发现的通用机器的描述集合中，我没有发现对这个问题的任何关注。如果不是为了停止问题，通用图灵机在任何对角线论点中是否有用？
终于我被 这是进一步的部分 在同一篇WP文章中，该文章说，戈德尔的不完整形式源于停止问题：“关于自然数的所有陈述的完整，一致和声音的公理化是无法实现的，其中“声音”应该是虚弱的。我知道，如果一个人不能得出矛盾，那么理论是一致的，并且关于自然数的完整理论似乎意味着关于自然数的所有真实陈述都可以在其中得出。我知道戈德尔说这种理论不存在，但是我看不出这样的假设的野兽可能是如何听起来不错的，即，也得出了对自然数字是错误的陈述：这种陈述的否定是真的，因此，通过完整性也可以衍生，这与一致性相矛盾。
我将感谢有关这些观点之一的任何澄清。
解决方案
我建议您检查Scott Aaronson的 博客文章 通过图灵机和罗瑟定理的不完整定理证明。他对不完整定理的证明非常简单且易于遵循。
其他提示
Neel Krishnaswami的答案 停止问题，不可兼容的集：常见的数学证明？ 在cstheory上 指向类别理论保护下连接上述结果的参考。
（这应该是Suresh回答的评论，但要适合那里太久了。因此，我事先表示歉意，这并不能真正回答Marc的问题。）
我发现Neel的答案 停止问题，不可兼容的集：常见的数学证明？ 在cstheory上 和 安德烈·鲍尔（Andrej Bauer）的博客文章 不满意的原因有两个。
首先，我们通常不需要所有类别理论行话来解释连接。不可决定的语言的存在是暗示的 坎托的定理, ，具有非常基本的对角线证明。原因是一组程序是等等到$ mathbb {n} $的。另一方面，由于每种语言都可以看作是$ mathbb {n} $的子集，因此所有语言的集合都是quinumeror to $ mathcal {p}（ mathbb {n}）$。根据Cantor的定理，从$ Mathbb {n} $到$ Mathcal {p}（ Mathbb {n}）$没有陈述，因此我们知道必须存在一种不可否认的语言。
其次，以上证明是不令人满意的，因为我们还想“查看”合理的不确定语言的示例。上面的证据可以看作是计数论点，因此在这种意义上并不是真正“建设性”。图灵发现了停止问题，例如这样一个例子。
“如果不是为了停止问题，通用图灵机在任何对角线上是否有用？”
稻的定理本质上是对角色机器对角化机的概括。它表明，除非该属性为所有图灵机或没有图灵机器都保留，否则绝对没有关于图灵机的属性。请注意，所有图灵机或没有图灵机的属性持有的属性可防止对角度化对象是图灵机器，因此首先不能在列表中与有关该属性的决定矛盾。的确，这是 只要 防止对角度化对象在列表上并与该财产的决定相矛盾的事情，这是图灵机的所有属性。对角度化对象的这种模式需要成为您试图做出决定的事物列表的成员，但否定了决定，是劳维尔定理（Suresh答案中的链接中引用）捕获的关键抽象为了充分概括对角的概念。现在，由于我们通过经验知道，几乎每个对角线化似乎都具有导致数学逻辑中一些极为重要的结果的共同特性，这使劳维尔定理成为有趣的工具。
