注意：我对哥德尔定理的经验非常有限：我读过哥德尔·埃舍尔·巴赫；略读了哥德尔定理导论的上半部分（彼得·史密斯著）；还有一些在互联网上随处可见的东西。也就是说，我对理论只有一个模糊的高级理解。
在我看来，哥德尔的不完备性定理（以及它的许多相关定理，例如停机问题和 Löbs 定理）是最重要的理论发现之一。
然而，观察到没有那么多（至少据我所知）定理的理论应用，这有点令人失望，这可能部分是由于 1. 证明的钝性 2. 人们没有强烈的哲学含义' t 愿意轻易承诺。
尽管如此，仍有一些尝试将这些定理应用于心灵哲学/人工智能环境中。在我的头顶上：
Lucas-Penrose Argument：它认为思想不是在正式系统（如计算机）上实现的。（但不是一个非常严格的证明）
显然，MIRI 的一些研究使用了 Löbs Thereom，尽管我知道的唯一例子是Löbian 代理合作。
这些都很酷，但是还有更多的例子吗？尤其是那些真正被学术界认真考虑的。
人工智能肯定有很多影响，包括：
一阶逻辑的推理是半可判定的。对于所有想要将逻辑用作主要 AI 工具的人来说，这是一个很大的失望。
两个一阶逻辑语句的基本等价是不可判定的，这对基于知识的系统和数据库有影响。例如，数据库查询的优化因此是一个无法确定的问题。
两个上下文无关文法的等价性是不可判定的，这是语言处理的形式语言学方法的一个问题
在 AI 中进行规划时，对于一些在实践中需要的规划语言来说，仅仅找到一个可行的计划是无法确定的。
在进行自动程序生成时 - 我们面临着一堆可判定性结果，因为任何合理的编程语言都与图灵机一样强大。
最后，关于表达性计算范式的所有重要问题，例如 Perti 网或元胞自动机，都是不可判定的。
我在阅读以下 Wikipedia 文章时，在Gödel 的 1951 年 Gibbs 关于不完备性定理的某些哲学后果的讲座中发现了数学家和哲学家Solomon Feferman的这篇论文
他的摘要（正如预期的那样）为我们提供了对同一讨论内容的高级概念：
这是对哥德尔 1951 年吉布斯关于不完备定理的某些哲学后果的演讲的第一部分的批判性分析。
哥德尔的讨论是以客观数学和主观数学的区别为框架的，根据这种区别，前者由绝对意义上的数学真理组成，后者由所有人类可证明的真理组成。
问题是这些是否一致；如果他们这样做了，那么没有正式的公理系统（或图灵机）可以理解人类思想的数学化潜力，如果不是，那么就存在绝对无法解决的丢番图形式的数学问题。
要么……人类的思想……无限超越任何有限机器的能力，要么存在绝对无法解决的丢番图问题。
至少在哲学上，这可能对人工智能的研究很感兴趣。恐怕这篇论文可能与您链接到的关于卢卡斯和彭罗斯哲学“尝试”或论点的文章相似。
大约 20 年前，我在这方面写了一篇详尽的文章，发表在《人工智能的工程应用》 12 (1999) 655-659 上。这是相当技术性的，你可以在我的个人网站上完整阅读，但这是结论：
上面显示了哥德尔定理有无限多的证明结构——与迄今为止在人工智能讨论中使用的单一证明结构形成鲜明对比。虽然所有实际公开的结构都可以被计算机模仿，但显然还有尚未公开的结构。我们的分析表明，可能存在只有人类才能发现的结构。这是一个很小且绝对无法证明的“可能”，取决于人类想象力的极限。
因此，争论人和机器在数学上的等价性的人最终必须依赖于他们对有限思维的信念，这意味着他们的结论包含在他们的假设中。另一方面，提倡人类优越性的人必须在他们的数学论证中假设这种优越性，最终只能得出从一开始就已经存在于他们的推理系统中的结论。
因此，如果不对人类思维做出假设，同时也是论证的结论，就不可能产生关于人类思维与图灵机之间关系的（元）数学上合理的论证。因此，这件事是无法确定的。
免责声明：从那以后我就离开了学术界，所以我不知道当代思想。