哥德尔不完备定理 incompleteness theorems (Panu Raatikainen)

首次发表于 2013 年 11 月 11 日星期一;实质性修订于 2020 年 4 月 2 日星期四。

哥德尔的两个不完备定理是现代逻辑中最重要的结果之一,对各种问题有深远的影响。它们涉及形式公理理论中可证明性的限制。第一个不完备定理指出,在任何一致的形式系统 F 中,可以进行一定数量的算术运算,F 的语言中存在无法在 F 中证明或证伪的陈述。根据第二个不完备定理,这样一个形式系统无法证明系统本身的一致性(假设它确实是一致的)。这些结果对数学和逻辑的哲学产生了巨大影响。人们还试图将这些结果应用于其他哲学领域,如心灵哲学,但这些尝试的应用更具争议。本文概述了这两个不完备定理及其周围的各种问题。(有关哥德尔的不完备定理的讨论,请参见 Kurt Gödel 的条目,将其置于他的数学和哲学工作的更广泛讨论的背景中。)


1. 引言

1.1 概述

哥德尔不完备定理是现代逻辑学中最重要的结果之一。这些发现彻底改变了对数学和逻辑的理解,并对数学哲学产生了重大影响。也有人试图将它们应用于其他哲学领域,但许多这样的应用的合法性更具争议性。

要理解哥德尔的定理,首先必须解释与之相关的关键概念,如“形式系统”、“一致性”和“完备性”。大致而言,形式系统是一套公理和推理规则的系统,允许生成新的定理。公理集合要求是有限的或至少可判定的,即必须存在一种算法(有效方法),使得可以机械地判断给定的陈述是否是公理。如果满足这个条件,该理论被称为“可递归公理化”,或者简称为“公理化”。形式系统的推理规则也是有效的操作,这样就可以始终机械地判断是否存在一个合法的推理规则应用。因此,对于任何给定的有限公式序列,都可以判断它是否构成系统中的真正推导或证明——给定系统的公理和推理规则。

如果一个形式系统对于系统的语言中的每个陈述,要么该陈述要么其否定可以在系统中推导出(即被证明),那么该形式系统是完备的。如果不存在这样的陈述,使得该陈述本身及其否定都可以在系统中推导出,那么该形式系统是一致的。在这个背景下,只有一致的系统才具有任何兴趣,因为逻辑的基本事实是,在一个不一致的形式系统中,每个陈述都是可推导的,因此,这样的系统是显然完备的。

哥德尔建立了两个不同但相关的不完备定理,通常称为第一不完备定理和第二不完备定理。“哥德尔定理”有时用来指代这两个定理的合并,但也可以单独指代其中之一,通常是第一个。根据 J. Barkley Rosser 在 1936 年的改进,第一个定理可以粗略地陈述如下:

第一不完备定理 在任何一致的形式系统 F 中,可以进行一定数量的初等算术,但该系统是不完备的;即,在 F 的语言中存在无法在 F 中被证明或证伪的陈述。

哥德尔不完备定理并不仅仅声称存在这样的陈述:哥德尔证明的方法明确地产生了一个在 F 中既不可证明也不可证伪的特定句子;这个“不可判定”的陈述可以从对 F 的规范机械地找到。所讨论的句子是一个相对简单的数论陈述,一个纯粹的普遍算术陈述。

一个常见的误解是将哥德尔的第一定理解释为显示存在无法证明的真理。然而,这是不正确的,因为不完备定理并不涉及任何绝对意义上的可证性,而只涉及某个特定形式系统中的可导性。对于在特定形式系统 F 中无法证明的任何陈述 A,显然存在其他形式系统,在这些系统中 A 是可证的(将 A 作为公理)。另一方面,存在着极为强大的标准公理系统泽尔梅洛-弗兰克尔集合论(简称 ZF,或者带有选择公理的 ZFC;请参见集合论条目中关于 ZFC 公理的部分),它足以推导出所有普通数学。现在根据哥德尔的第一定理,甚至在 ZFC 中也存在着无法证明的算术真理。证明它们将需要一个超越 ZFC 的方法的形式系统。因此,在今天的“普通”数学方法和公理下,这样的真理在某种意义上是无法证明的,也不能以数学家今天认为毫无问题和决定性的方式证明它们。

哥德尔的第二不完备定理涉及一致性证明的限制。一个粗略的陈述是:

哥德尔不完备定理二 对于任何一致的系统 F,其中可以进行一定数量的初等算术运算,在 F 本身中无法证明 F 的一致性。

在第二个定理的情况下,F 必须包含比第一个定理的情况下更多的算术,第一个定理在非常弱的条件下成立。需要注意的是,这个结果和第一个不完备定理一样,是关于形式可证性或可推导性的定理(这总是相对于某个形式系统来说的;在这种情况下,相对于 F 本身)。它并不说明对于满足定理条件的特定理论 T,陈述“T 是一致的”是否可以通过确凿的论证或者对数学家普遍接受的证明来证明为真。对于许多理论来说,这是完全可能的。

1.2 一些形式化理论

不完备理论的存在并不令人惊讶。取任何一个理论,即使是一个完备的理论(见下面的例子),去掉一些公理;除非这个公理是多余的,否则得到的系统就是不完备的。然而,不完备定理处理的是一种更为根本的不完备现象。与上述那种显然不完备的理论不同,可以很容易地完成,相关理论无法完成;所有它们的扩展,只要它们仍然是形式系统,因此可公理化,也是不完备的。它们可以说是“本质上不完备的”。

在上面给出的不完备定理的第一种和宽泛的陈述中,出现了“可以进行一定数量的初等算术”的模糊要求。现在是时候把这个要求更加明确化了。

1.2.1 算术理论

在不完备性和不可判定性方面通常被考虑的最弱标准算术系统是所谓的罗宾逊算术(由拉斐尔·M·罗宾逊提出;参见塔斯基、莫斯托夫斯基和罗宾逊,1953 年),标准记作 Q。作为公理,它有以下七个假设:

  • ¬(0=x′)

  • x′=y′→x=y

  • ¬(x=0)→∃y(x=y′)

  • x+0=x

  • x+y′=(x+y)′

  • x×0=0

  • x×y′=(x×y)+x

“x′” 的预期解释是后继函数,而且显然,“+” 和 “×” 分别是加法和乘法函数。“0” 是唯一的常数,表示零。

在这些基本公理的基础上,还添加了归纳公理方案:

(IND)ϕ(0)∧∀x[ϕ(x)→ϕ(x′)]→∀xϕ(x),

结果在(一阶)皮亚诺算术(PA)中。请注意,与 Q 不同,PA 包含无限多个公理,因为将语言中至少有一个自由变量的每个公式 ϕ(x)的所有(无限多个)归纳方案实例都作为公理。但是,检查给定句子是否是此方案的实例是一项例行机械任务。PA 通常被视为标准的一阶算术系统。

另一个自然且广泛研究的算术系统,介于 Q 和 PA 之间的强度,是原始递归算术(PRA)。它不仅包含了控制后继、加法和乘法的 Q 的上述公理,还包含了所有原始递归函数的定义公理(参见递归函数条目),并且归纳方案的应用仅限于无量词公式(即,ϕ(x)不允许包含任何(无界的)量词)。

然而,如果只采用 Q 的公理和归纳方案限制在大致上纯存在量词公式(在技术术语中为 Σ01-公式;见下文)(这是由 Parsons 1970 首次证明的),则可以得到基本相同的系统。此外,可以证明 Σ01-归纳(Paris 和 Kirby 1978)等价于归纳方案限制在(大致上)纯全称公式(Π01-公式)。PRA 也可以被表述为“无逻辑”的等式演算。PRA 或等效于 PRA 足以发展形式化理论的语法理论。它通常被视为在其中研究各种其他系统的无问题背景理论,这些系统的合法性可能更具争议。

比 PA 更强大的系统,在数学基础中非常重要,下面会不时提到,是二阶算术 PA2(也经常用 Z2 表示)。它足以发展所有普通的分析和代数。它的语言是一个双排序的一阶语言(参见二阶和高阶逻辑的条目),即它包含两种变量类型,数字变量 x1,x2,…(或 x,y,z,…)和属性变量 X1,X2,…(或 X,Y,Z,…),其中属性是外延概念。作为公理,除了 PA 的基本公理外,它还包括二阶包含方案的所有实例:

∃X∀x[Xx↔ϕ(x)]

其中 ϕ(x)可以是 PA2 语言中的任何公式,其中 X 不自由出现。(值得一提的是,PA2 也可以通过将集合成员关系(∈)作为原始概念添加到语言中,将变量 X,Y,Z,…明确地视为集合范围,并将二阶包含重新表述为 ∃X∀x[x∈X↔ϕ(x)]。)

PA2 是一个非常强大的理论。通过解释方法(见下文),可以证明它在证明论上与没有幂集公理的策梅洛-弗兰克尔集合论 ZFC-Pow 一样强大(而标准的一阶 PA 在证明论上与没有无穷公理的 ZFC-Inf 等价)。 (参见集合论条目中关于 ZFC 公理的部分。)

显然,我们假设我们的形式系统也配备了一套推理规则(可能还有一些逻辑公理),通常是一些标准的经典逻辑系统(尽管不完备定理本质上不预设经典逻辑,也适用于具有直觉主义逻辑等的系统)。所有上述标准系统都带有经典逻辑。标准符号 F⊢A 用于表示(在元层次上)A 在 F 中是可导出的,即在 F 中有一个 A 的证明,或者换句话说,A 是 F 的一个定理。相应地,F⊬A 表示 A 在 F 中不可导出。

总结一下:在不完备定理的背景下,当说“在一个系统中可以进行一定数量的初等算术”时,通常意味着它包含 PRA 或至少 Q。对于第一个不完备定理,Q 是足够的;对于第二定理的标准证明,至少需要类似 PRA 的东西。有一个关于 Q 的第二不完备定理的版本(参见 Bezboruah&Shepherdson 1976),但关于 Q 中的相关陈述是否真的可以表达一致性存在一些争议,因为 Q 太弱(参见 Kreisel 1958; Bezboruah&Shepherdson 1976; Pudlák 1996; Franks 2009)。

1.2.2 不是用算术语言表达的理论

当然,数学中有许多重要且有趣的理论甚至没有用算术语言来表达。然而,当注意到不完备定理的适用性可以在一阶算术语言及其扩展之外得到显著扩展时,可以发现只需要弱理论(如 Q 或 PRA)可以在所讨论的系统中进行解释。最重要的是,这涉及到各种集合论系统。例如,不完备定理适用于 ZFC-Inf(即没有无穷公理的 ZFC)及其所有扩展,只要它们是可公理化的。

粗略地说,如果理论 T1 的原始概念和变量的范围可以在理论 T2 中定义,那么理论 T1 就可以在理论 T2 中进行解释,这样就可以将 T1 的每个定理翻译成 T2 的定理。不应将这种解释误解为提供任何直观的同义词性。两个理论可能具有根本不同的预期主题,但作为形式系统,一个理论可能在另一个理论中进行解释。(举个例子:一个关于祖先的简单理论可以作为一个形式系统,在算术中进行解释;显然,这并不意味着祖母之类的东西真的是数字。)重要的是,解释保留了理论的某些基本形式属性,尤其是一致性:如果 T1 在 T2 中可以解释,并且 T2 是一致的,那么 T1 也是一致的。而且,任何可以解释 Q 的系统都保证是本质上不完备的。对于任何这样的理论,其中 Q 可以解释,不完备性也可以直接证明;例如,在各种集合论理论中,可以通过集合(称为“哥德尔集”)编码公式和推导(而不是数字),然后按照通常的方式进行推导(参见,例如,Fitting 2007)。然而,对于大多数目的来说,更简单的方法是在所讨论的理论中建立 Q 的可解释性。

总之,当说“在一个系统中可以进行一定数量的初等算术”时,意思是该系统是 Q 的可公理化扩展,或者 Q 可以在其中进行解释。(在(第二个不完备性定理的标准证明中),将 PRA 替换为 Q。)

1.2.3 一些例外情况:完全理论

另一方面,并非所有的算术理论都是不完备的。例如,仅涉及自然数加法而不涉及乘法的理论(通常称为“普雷斯伯格算术”)是完备的(且可判定)(普雷斯伯格,1929 年),正整数乘法的理论也是完备的(斯科勒姆,1930 年)。尽管这些理论非常弱,但无论如何,至少需要一个同时涉及加法和乘法的理论。更有趣的是,涉及实数的自然一阶算术理论(同时涉及加法和乘法),即所谓的实闭域理论(RCF),既是完备的又是可判定的,这是由塔斯基(1948 年)证明的;他还证明了欧几里得几何的一阶理论是完备的和可判定的。因此,应该记住,存在一些非平凡且有趣的理论,哥德尔的定理不适用于这些理论。

1.3 Church-Turing 论题的相关性

哥德尔最初只证明了一个特定但非常全面的形式化理论 P 的不完备性,这个理论是罗素的类型理论系统 PM 的变体(参见关于类型理论和 Principia Mathematica 的条目中关于悖论和罗素的类型理论的部分),以及具有相同语言的 P 的所有扩展,其公理集是原始递归的。他还提出了,尽管没有证明,该证明可以适应于集合论的标准公理系统,如 ZFC。尽管事实证明哥德尔实际上已经有了一个非常普遍的结果,但当时并不清楚这个结果有多普遍(另见第 5 节)。

仍然缺少的是对可决定性直观概念的分析,这在对任意形式系统的概念进行表征时是必需的。回想一下,公理集和形式化系统的证明关系需要是可决定的。数学家和逻辑学家自古以来一直隐含地使用决策方法的直观概念,只要要求一个正解,只要提供一个直观上被每个人认为是机械方法的具体方法就足够了。然而,对于一般的限制性结果,如一般的不完备定理或不可决定性结果(见 4.2),需要对该概念进行精确的数学阐释。人们经常考虑有效或可计算的函数或操作,而不是可决定的集合或属性,但实际上这只是同一个问题的两个方面——对其中一个的讨论可以很容易地转录为对另一个的讨论。

哥德尔(1934 年),阿隆佐·邱奇(1936a,b)和艾伦·图灵(1936-7)独立提出了对可计算函数(以及可决定的数集)的精确数学定义的不同建议,结果证明这些建议都是等价的。图灵的仔细概念分析使用了虚构和抽象的计算机(现在通常称为“图灵机”;请参阅图灵机条目),这一点特别重要,正如哥德尔本人强调的那样(见,例如,哥德尔 1963)。直观概念和其中一些数学阐释的等式通常被称为“邱奇-图灵论题”。出于历史原因,“递归函数”这个标签在逻辑文献中占主导地位。因此,可决定的集合通常被称为“递归集合”。(请参阅可计算性、递归函数和邱奇-图灵论题条目。)

为了正确理解不完备性和不可判定性的结果,理解关于集合的两个关键概念之间的区别至关重要。首先,可能存在一种机械方法,可以决定任何给定的数字是否属于所讨论的集合(在这种情况下,该集合被称为“可判定的”或“递归的”),其次,可能存在一种机械方法,逐个生成或列出集合的元素。在后一种情况下,该集合被称为“可递归枚举的”(r.e.),也就是说,它可以被有效地生成,或者说它是“半可判定的”。这是可计算性理论(或“递归函数理论”)的一个基本结果,即存在可递归枚举的集合,这些集合可以被有效地生成(即可递归枚举),但不能被判定(即不是递归的)。实际上,在非常抽象的层面上,这就是第一个不完备性定理的本质。然而,如果一个集合及其补集都是可递归枚举的,则该集合是递归的,即可判定的。

2. 哥德尔不完备定理

在本节中,概述了第一个不完备性定理的证明主要线索。对于对更多细节感兴趣的读者,可以参考补充材料(哥德尔编号和对角线引理)。

2.1 准备工作

正式术语(“数字”)规范地表示自然数 n 的简写为 n––。在这里使用的算术标准语言中,数字 n 用术语 0′⋯′表示,其中继承符号‘′’被迭代 n 次。也就是说,表示 1、2、3 等数字的数字是 0′、0′′、0′′′,并且简写为 1、2、3 等。

在他最初的证明中,哥德尔使用了他特定的 ω-一致性概念,对于某些目的来说,遵循哥德尔的原始方法仍然很方便。如果一个形式化理论 F 是 ω-一致的,那么对于某个公式 A(x),既有 F⊢¬A(n––)对于所有 n,又有 F⊢∃xA(x)不成立。这自然地意味着正常一致性,并且是基于自然数满足 F 的公理的假设。

实际上,在这里只需要一个简单的特殊情况的 ω-一致性;即,这个假设只需要与逻辑学家所称的 Σ01-公式有关;这些公式大致上是纯存在的公式;更确切地说,是形如 ∃x1∃x2…∃xnA 的公式,其中 A 不包含任何无界量词(A 可能包含有界全称量词 ∀x < t 和有界存在量词 ∃x < t)。这种受限的 ω-一致性被称为 1-一致性。

ω-一致性和 1-一致性是纯语法概念。如果允许使用真假概念,那么 1-一致性的假设可以直观地表达为所讨论的形式系统不证明任何假的 Σ01-句子(即,至少在这些句子的情况下,该系统是完备的)。从现在开始,假设所考虑的形式化系统包含 Q,并且至少是 1-一致的,除非另有说明。

2.2 可表示性

哥德尔的证明还需要在形式系统 F 中表示集合和关系的概念。更确切地说,需要两个相关的概念。

如果存在一个具有一个自由变量 x 的 F 语言的公式 A(x),使得对于每个自然数 n,自然数集合 S 在 F 中强表示,则集合 S 在 F 中强表示。

n∈S⇒F⊢A(n––); n∉S⇒F⊢¬A(n––),

如果存在 F 语言的公式 A(x),使得对于每个自然数 n,n∈S⇔F⊢A(n––),那么自然数集合 S 在 F 中是弱可表示的。

对于多元关系,这些概念的推广是显而易见的。函数的可表示性也有相关概念。正如不完备性定理特别教导我们的那样,存在一些集合只是弱可表示而不是强可表示(其中一个关键例子是系统中可证明的陈述的集合)。

It is obvious how all these notions are generalized to many-place relations. There are also related notions of representability for functions. As the incompleteness results in particular teach us, there are sets which are only weakly but not strongly representable (the key example being the set of statements provable in the system).

[警告:这里文献中的术语变化很大:“强表示”有时被称为“表示”,“逐数字表达”,“双数字表达”,“定义”或“强定义”;而“弱表示”则可以用“表示”,“定义”,“弱定义”或“数字表达”来表示。在这里应该小心,并专注于相关定义,不要让词语误导。]

对于弱表示和强表示的两种情况,总是存在一个简单的存在性 Σ01 公式,它(弱或强)表示所讨论的集合,并且通常使用这样的公式来表示 S。

尽管这些概念是相对于形式系统的,但事实证明,强表示和弱表示非常稳定。无论选择哪个特定的形式系统,只有可判定的或递归的集合(关系)才能被强表示,而只有半可判定的或可递归枚举的集合(关系)才能被弱表示。这适用于包含罗宾逊算术 Q 的所有形式化系统,从罗宾逊算术本身到像 ZFC 和更强的集合论公理系统(只要它们是(可递归)公理化的)。哥德尔没有使用“表示性”的概念,而是采用了一种不同的方法,即讨论集合在形式系统 F 中是否“可判定”(“entscheidungsdefinit”)。如果 F 的证明是系统地生成的,那么对于任何给定的数字 n,最终将确定它是否属于 S——前提是 S 在 F 中是强表示的。

总之,我们有:

可表示性定理 在任何包含 Q 的一致形式系统中:

  1. 如果且仅如果一个集合(或关系)是递归的,那么它是强可表示的;

  2. 如果且仅如果一个集合(或关系)是可递归枚举的,那么它是弱可表示的;

表示性的这两个概念——强表示性和弱表示性——必须与仅仅可定义性(按照标准意义的定义)明确区分开来。如果在算术语言中存在一个公式 A(x),使得在自然数的标准结构(预期的解释)中 A(n––)为真,当且仅当 n∈S,那么集合 S 在算术语言中是可定义的。有许多集合可以在算术语言中被定义,但不能(甚至是弱地)在任何 F 中表示,例如一致公式的集合、系统 F 中不可证明的句子的集合,或者没有解的丢番图方程的集合(见下文)。

2.3 正式语言的算术化

Gödel 证明的下一个关键步骤是将形式系统的语言进行算术化处理,这个语言总是被准确定义的(这是形式系统的一部分),并且在该语言的表达式和自然数系统之间建立一种特定类型的对应关系——语言的编码、“算术化”或“哥德尔编号”。有许多可能的方法来实现这一点,细节并不重要(有关一种相当标准的方法的更多细节,请参阅附加文档《哥德尔编号》)。关键点在于所选择的映射是有效的:从一个表达式到其代码编号,以及从一个数字到相应的表达式,总是可以纯机械地进行。如今,当我们大多数人都熟悉计算机,并且许多事物都可以用 0 和 1 进行编码时,这种算术化的可能性几乎是不足为奇的。

粗略地说,步骤如下:首先,将语言的原始符号与不同的自然数配对,即“符号编号”。然后,一些数论知识足以通过单个数字对数字序列进行编码。因此,作为原始符号序列的良好形式的公式被分配一个唯一的数字。最后,系统的推导或证明,作为公式序列,被进行算术化处理,并且也被分配特定的数字。这样的编码,即公式 A 的“哥德尔编号”,表示为 ┌A┐,对于推导也是如此。

通过这种方式,语法属性、关系和操作在算术中得到反映:例如,neg(x)是将一个公式的哥德尔数发送到其否定的算术函数;换句话说,neg(┌A┐)=(┌¬A┐);类似地,impl(x,y)是将一对公式的哥德尔数映射到公式蕴含的哥德尔数的函数:impl(┌A┐,┌B┐)=┌A→B┐;等等。存在一个算术公式,称为 Fmla(x),当且仅当 n 是系统中一个良构公式的哥德尔数时,该公式对 n 为真。还存在一个算术公式 M(x,y,z),当且仅当对于某些公式 A 和 B,具有 x=┌A┐,y=┌A→B┐ 和 z=┌B┐ 时,可以有效地应用推理规则 modus ponens;等等。通过这种方式,所有的语法属性和操作都可以在数字层面上模拟,而且它们在包含 Q 的所有理论中都是强表示的。

由于(根据形式系统的定义)判断给定的公式序列是否构成给定句子的证明是可判定的,根据所选择的形式系统 F 的规则,二元关系“x 是(哥德尔数为)公式(的证明)(具有哥德尔数)y”可以在包含 Q 的所有系统中强表示,特别是在 F 中。让我们用 PrfF(x,y)来表示在 F 本身中强表示这个关系的公式。在 F 中可证明的性质可以定义为 ∃xPrfF(x,y)。让我们将这个形式化的可证性谓词缩写为 ProvF(x)。由此可知,后者是弱表示的(尽管事实证明,它不是强表示的):

F⊢A⇒F⊢ProvF(┌A┐)。

总是可以选择可证性谓词 ProvF(x)为一个 Σ01-公式。

2.4 对角线化,或者说“自指”

Gödel 证明的下一个,也许有些令人惊讶的重要引理是以下引理(我们仍然假设 F 是一个包含 Q 的形式系统):

对角线引理

设 A(x) 是 F 语言中只有一个自由变量的任意公式。那么可以机械地构造一个句子 D 使得 F⊢D↔A(┌D┐) 成立。

哥德尔不完备定理

(有关证明的概述,请参见补充:对角线引理)

在文献中,这个引理有时也被称为“自指引理”或“不动点引理”。它在不完备定理之外还有许多重要的应用。

通常说,对于由 A(x)表示的性质,句子 D 是一个自指句子,它“自称”具有性质 A。这样的修辞手法在启发上可能有用,但也很容易引起误导并暗示过多。例如,注意该引理仅在 D 和 A(┌D┐)之间提供了(可证明的)物质等价关系(即两边必须具有相同的真值),并不声称任何意义上的相同。特别地,D 和 A(┌D┐)绝不相同,┌D┐ 和 ┌A(┌D┐)┐ 也不相同。

2.5 哥德尔不完备定理一——证明完成

为了完成证明,对否定的可证性谓词 ¬ProvF(x)应用对角线引理:这给出了一个句子 GF,使得

(G)F⊢GF↔¬ProvF(┌GF┐)。

因此,甚至在 F 内部也可以证明,如果 GF 为真,则 GF 在 F 中不可证明。

如果 F 只是 1-一致的,那么很容易证明 GF 既不可证明也不可证伪。

对于前半部分,假设 GF 是可证明的。那么,由于 F 实际上也证明了_provability-in-_ F 的弱可表示性,即 F 也会证明 ProvF(┌GF┐)。然而,因为 F 实际上还证明了等价性(G),即 F⊢GF↔¬ProvF(┌GF┐),所以 F 也会证明 ¬GF。但这意味着 F 是不一致的。总之,如果 F 是一致的,则 GF 在 F 中不可证明。对于这个前半部分,F 的简单一致性的假设就足够了。

对于后半部分,必须假设 F 是 1-一致的(如果选择了 ProvF(┌GF┐)使其成为 Σ01-句子,则需要更一般的假设 ω-一致性)。

假设 F⊢¬GF。那么 F 不能证明 GF,否则 F 将变得不一致。因此,没有自然数 n 是 GF 的证明的哥德尔数,而且由于证明关系是强表示的,对于所有 n,F⊢¬PrfF(n––,┌GF┐)。如果还有 F⊢∃xPrfF(x,┌GF┐),则 F 不是 1-一致的,与假设相矛盾。因此,F 不证明 ∃xPrfF(x,┌GF┐),换句话说,根据 ProvF(x)的定义,F 不证明 ProvF(┌GF┐)。根据关键等价性(G),F 也不证明 ¬GF。

哥德尔不完备定理

假设 F 是一个包含罗宾逊算术 Q 的形式化系统。那么可以从 F 中机械地构造出 F 的语言的一个句子 GF,使得:

  1. 如果 F 是一致的,那么 F⊬GF。

  2. 如果 F 是 1-一致的,那么 F⊬¬GF。

这样一个独立的、或者说是“不可判定的”(即在 F 中既不可证明也不可证伪的)陈述 GF 在 F 中通常被称为“哥德尔句子”。

实际上,在有利的情况下,可以证明如果 F 确实是一致的,那么 GF 是真的。例如,如果可证性谓词 ProvF(x)被选择为 Σ01-公式:那么哥德尔句子可以被证明等价于全称公式 ∀x¬PrfF(x,┌GF┐)。这样的公式在事实上为假时可以被证明为假:如果为假,那么就会存在一个数 n 使得 F⊢PrfF(n––,┌GF┐)(这在 Q 中已经成立)。然而,这将与不完备定理相矛盾。因此,GF 不能为假,必须为真。因此,哥德尔句子通常被称为“真但不可证明”。

在这里不应该混淆:“哥德尔定理”是哥德尔的一般不完备性结果,涉及到一大类形式系统,而“哥德尔句子”是构造的、形式上不可判定的句子,它在不同的形式系统中是不同的。这就是为什么在 GF 中包含下标 F 是重要的原因。此外,在这个背景下,不应该混淆“不可判定”这两个不同的意义。一方面,一个特定的句子,如哥德尔句子,可能在被选择的系统中是独立的,即既不可证明也不可证伪。另一方面,一个理论可能是不可判定的(见下文),意味着不存在一种决策方法来确定语言中的任意给定句子是否可在该理论中推导出来(因此,“不可判定”的这个后一种意义涉及了一个无限类的陈述,可以这么说)。

在对第一不完备定理的非正式解释中,经常说哥德尔句子 GF“说它自己是不可证明的”。然而,这样不准确的陈述至少应该带有一些保留态度。有很多理由可以得出结论,至少在一般情况下,哥德尔句子并没有真正关于自身的实质性陈述(Milne 2007 对此类问题进行了仔细分析);例如,在对角线引理的情况下,通常在这里使用的是纯粹的物质等价关系。

罗瑟改进——从 ω-一致性到一致性

1936 年,巴克利·罗瑟(J. Barkley Rosser)进行了一项重要改进,允许在哥德尔第一定理的证明中摆脱有些笨拙的 ω-一致性假设。为此,罗瑟引入了一个新的、有些人为的“可证明谓词”Prov∗(x),其非正式构造如下:

存在一个 y,使得 y 是具有 Gödel 编号 x 的公式的证明的 Gödel 编号,并且不存在比 y 更小的 z,使得 z 是具有 Gödel 编号 x 的否定公式的证明的 Gödel 编号。

更正式地说:

Prov∗(x)=def∃y[PrfF(y,x)∧∀z < y(¬PrfF(z,neg(x)))],

其中 PrfF(y,x)是前面讨论过的更标准的证明关系。

恰好,如果所考虑的形式系统 F 确实是一致的,Rosser 的可证性谓词与普通的可证性谓词是同扩展的。将对 Rosser 的可证性谓词 Prov∗(x)的否定应用对角线引理得到:

Rosser 对第一个定理的修改(Rosser 1936) 设 F 是一个包含 Q 的一致形式化系统。那么存在一个 F 的语言中的句子 RF,使得 F 中既不能证明 RF,也不能证明 ¬RF。

2.6 不完备性和非标准模型

从模型论的角度来看,对第一个不完备性定理进行反思是很有启发的,尽管定理本身并不需要这样做。换句话说,可以得出结论,满足定理条件的任何理论 F 都必须除了预期的解释或“标准模型”(在算术理论的情况下,即自然数的结构)之外,还具有非预期的解释或“非标准模型”——没有这样的理论可以排除后者并唯一确定预期的解释。换句话说,如果存在独立的陈述,如 GF,F 必须既具有满足 GF 的模型,也具有更满足 ¬GF 的模型。由于 ¬GF 等价于 ∃xPrfF(x,┌GF┐),后者的模型必须具有满足公式 PrfF(x,┌GF┐)的实体。然而,我们知道(因为 PrfF(x,y)强烈地表示证明关系),对于任何数字 n––,F 可以证明 ¬PrfF(n––,┌GF┐)。因此,没有自然数 n 可以证明该公式。由此可见,任何这样的非标准模型必须在自然数(表示数字 n––的指称)之后包含“无限”的非自然数。

非标准模型的研究并不是从哥德尔的结果开始的 - 斯科勒姆特别早在不同的背景下就已经意识到了它们(他在 1922 年发现了集合论的一阶理论具有不自然地小的模型,即可数模型,参见斯科勒姆悖论的条目),但第一个不完备定理阐明了非标准模型在算术背景下的存在,而非标准模型阐明了第一个不完备定理。非标准模型此后成为数理逻辑中一个丰富的研究领域(参见,例如,Boolos 和 Jeffrey 1989 年:第 17 章;Kaye 1991 年)。

3. 第二个不完备定理

3.1 预备知识

从非正式的角度来看,导致第二不完备定理的推理相对简单。给定算术化的可证性谓词,也很容易提出一个算术化的一致性陈述:选择一些明显不一致的公式(在算术理论中,标准选择是(0–=1–));让我们用 ⊥ 表示它;系统的一致性(算术化的对应物)可以定义为 ¬ProvF(┌⊥┐)。让我们用 Cons(F)来缩写这个公式。第一不完备定理的第一部分的证明(即上面的情况(i))可以在 F 内部被形式化(实际上这肯定会很复杂)。这给出了:

F⊢Cons(F)→GF,

其中 GF 是第一个定理为 F 提供的哥德尔句子。如果 Cons(F)在 F 中是可证的,那么 GF 也是可证的,根据简单逻辑。这将与哥德尔的第一个定理相矛盾。因此,Cons(F)在 F 中也不能被证明。

哥德尔的第二不完备定理 假设 F 是一个包含初等算术的一致形式化系统。那么 F⊬Cons(F)。

这里有一个在哲学上很重要的问题应该提到:按照目前的说法,哥德尔的第二不完备定理只能证明一个句子 Cons(F)的不可证明性。但是这个句子真的表达了 F 的一致性吗?(将此与上面的备注进行比较,GF 严格来说并没有表达自己的不可证明性。)此外,可能还有其他可证明且表达了 F 一致性的句子吗?

给出第二定理的严格证明,以更一般的形式涵盖所有这样的句子,然而,事实证明这是非常复杂的。这样做的基本原因是,与第一定理不同,不仅仅是任何一个仅仅是外延充分的可证性谓词都适用于一致性主张的形式化。表达方式是有区别的。例如,上面提到的罗瑟的可证性谓词是不行的;如果一致性是用罗瑟的可证性谓词来表达的话,可以证明 F 在 F 中是“一致的”。因此,为了使第二不完备定理的证明能够进行下去,必须为可证性谓词添加一些进一步的条件。根据费弗曼(1960)的说法,习惯上说,第一定理及其相关定理是外延结果,而第二定理是内涵的:在某种意义上,必须能够认为 Cons(F)表达了 F 的一致性——它确实意味着 F 是一致的。

3.2 可导性条件

第二不完备定理的证明要求 F 中的可证性谓词满足一些在证明的细节中使用的条件。有几组不同的条件可以满足要求。

第二不完备定理的第一个详细证明出现在(希尔伯特和伯奈斯 1939 年)(主要由伯奈斯撰写),尽管只针对一个特定的理论,即 PA。它使用了一组相当笨拙的可证性谓词条件。这些条件更多是为了满足特定证明的需要,而不是对“自然”可证性谓词的任何分析。Löb(1955 年)提出了一套更加优雅、现在标准的“可导出条件”列表,尽管它们的预期用途有些不同(见下文)。

Löb 的可导出条件(D1)(D2)(D3)F⊢A⇒F⊢ProvF(┌A┐)。F⊢ProvF(┌A┐)→ProvF(┌ProvF(┌A┐)┐)。F⊢ProvF(┌A┐)∧ProvF(┌A→B┐)→ProvF(┌B┐)。

(D1)只是第一个定理证明中可证性是弱可表示的要求的重新表述。粗略地说,(D2)要求对于候选可证性谓词 ProvF 的整个证明,它本身可以在 F 内部形式化。最后,(D3)要求可证性谓词在演绎法则下是封闭的。

如果算术化的可证性谓词确实满足这些条件,那么第二个定理可以被证明。让 GF 再次成为第一个定理给出的 F 的哥德尔句子。使用可导性条件,很容易证明:

F⊢GF↔Cons(F)。

这立即导致了第一个不完备定理给出的 Cons(F)的不可证明性。

此外,Jeroslow(1973)通过一个巧妙的技巧证明了,实际上可以在没有(D3)的情况下建立第二个定理。然而,在某些其他情况下(例如,证明 Löb 的定理时;见下文),以及在可证性逻辑中,仍然需要满足所有三个条件。

3.3 Feferman 对第二个定理的替代方法

在假设一个理论的可证性谓词满足可导性条件(或者通过 Jeroslow 的技巧,至少满足 D1 和 D2)的前提下,相对容易证明第二个不完备定理的相关情况。然而,在实践中,人们必须逐个案例地确定所提出的算术化可证性谓词是否真正满足条件,而这通常是冗长而乏味的。

这个缺点,以及其他一些问题(参见 Feferman 1997),在 20 世纪 50 年代末,导致 Solomon Feferman 寻找了第二个定理的另一种攻击方式(参见 Feferman 1960)。Feferman 采取了两个步骤来解决这个问题:首先,他确定了 ProvFOL(x)这个公式,它将一阶逻辑中的某个标准可导性概念算术化,以便让我们能够在逻辑中固定一个选择的可证性公式。在这个阶段,关于所讨论的系统的非逻辑公理集合的呈现方式是开放的。其次,Feferman 寻找了适当的约束条件来呈现这些公理。在算术语言的公式中,他确定了他所称之为 PR-和 RE-公式;前者对应于算术中的规范原始递归(PR)定义,后者对应于前者的存在泛化。每个可递归可枚举(RE)集合都可以由后一类公式定义;这些就是 Σ01-公式。这两个类别在语法形式上很容易区分。(实际上,根据 MRDP 定理(见下文),人们可以将注意力从 RE-公式转移到更简单的存在量化丢番图方程的类别上。)

我们已经注意到一个重要事实,即在包含 Q 的所有算术理论 F 中,如果一个集合在 F 中强表示,那么它是递归的;而一个集合在 F 中递归可枚举,当且仅当它是弱表示的。此外,我们总是可以选择将表示该集合的公式为一个 RE 公式(即 Σ01 公式;并且根据 MRDP 定理,甚至是一个存在量化的丢番图方程)。因此,自然而然地要求所讨论的系统的非逻辑公理集由这样的公式表示。如果哥德尔数公理集的算术化定义反映了这些公理的归纳定义(如果是无穷的话),那么得到的公式将是 Σ01 的。(对于可以用有限公理公设的理论,公理集可以以列表的形式有唯一的表示,因此,相对于 ProvFOL(x)存在唯一的一致性陈述。)与确定可导性条件是否满足不同,确定形式化公理的给定公式是否确实具有所需的形式(Σ01)是一个相对常规的任务。

现在,Feferman 1960 年提出的第二不完备定理的版本是:

第二不完备定理的一个变体(Feferman 1960) 设 F 是 PA 的一致扩展,AxF(x)是一个弱表示 F 公理的 Σ01-公式,Cons(F)是由 AxF(x)和 ProvFOL(x)构造的一致性陈述。那么 Cons(F)在 F 中是不可证明的。

关于第二不完备定理的其他不同方法,请参见 Feferman 1982、1989a;Visser 2011。关于第二定理的一些哲学复杂性,请参见 Detlefsen 1979、1986、1990、2001;Auerbach 1985、1992;Roeper 2003;Franks 2009(另请参见 Hilbert 计划条目中关于不完备性的部分)。

4. 与不完备定理相关的结果

4.1 塔斯基关于真理不可定义性的定理

哥德尔首先通过观察系统中的真理(语言的真理)必须在系统中是不可定义的这一事实(参见下面的第 5 节)得出了不完备性的结果,这一结果通常归功于塔斯基(塔斯基在呈现这个问题上有一些真正的优点;参见 Gómez Torrente 2004)。现在让我们从塔斯基对真理的方法的背景下来看这个结果。

塔斯基明确区分了客体语言,即句子的真理受到质疑的语言,和用于讨论前者的元语言。他还要求(参见塔斯基的真理定义条目)任何对客体语言的真理 True(x)的令人满意的定义都应满足他的“T 公约”,即它应该具有所有形式为“T-等价”的等价关系作为其结果

(T)真(┌A┐)↔B,

其中 ┌A┐ 是目标语言的一个句子的名称,B 是它在元语言中的翻译。如果元语言与目标语言相同,或者是目标语言的扩展,那么 B 就是 A 本身,而 T-等价关系的形式为:

真(┌A┐)↔A.

哥德尔不完备定理表明的是,对象语言和元语言不能重合,而必须是不同的。

塔斯基的不可定义性定理 设 F 是一个包含足够数量算术的一致形式化系统。那么在 F 的语言中不存在一个公式 Tr(x),使得对于 F 的语言中的每个句子 A:

F⊢Tr(┌A┐)↔A.

证明思路:如果 F 的语言中存在这样的公式,将其否定应用于对角线引理,将会得到悖论句子 L(参见悖论句子),使得:

F⊢¬Tr(┌L┐)↔L,

与被假定为可推导的 T-等价性一起,这将迅速导致明显的矛盾,从而与 F 一致性的假设相矛盾。

同样地,可以证明 F 的真句集在 F 的预期解释中是不可定义的——按照现在的标准意义上的“可定义性”(见上文)。

4.2 不可判定性结果

证明哥德尔不完备定理所使用的工具还提供了各种重要的不可判定结果。如果一个理论是可判定的,那么它的定理集合(在其中可推导的句子)是可判定的,也就是说(根据丘奇-图灵论题)是递归的。否则,该理论是不可判定的。非正式地说,可判定意味着存在一种机械过程,使得可以判断任意给定的句子(属于该理论的语言)是否是定理。

如果一个理论是完备的,那么它是可判定的(证明概要:给定一个句子 A,系统地生成该理论的定理;根据完备性,最终会在有限时间内产生 A 或 ¬A)。然而,反过来并不总是成立:存在不完备但可判定的理论。尽管如此,不完备性至少打开了不可判定性的可能性。此外,所有包含罗宾逊算术 Q(直接包含或可以在其中解释 Q)的理论都是不完备且不可判定的。因此,对于非常广泛的理论类别,不完备性和不可判定性是相伴而行的。

一种证明 Q 的扩展不可判定性的优雅而简单的方法大致如下:设 F 是任何包含 Q 的一致理论。然后假设它的定理集合是可判定的,也就是说(根据丘奇-图灵论题)是递归的。那么就会得出结论,F 的定理(的哥德尔数的集合)在 F 本身中是强表示的。回想一下,这意味着存在 F 的语言中的某个公式 B(x),使得不仅当 F⊢A 时 F⊢B(┌A┐)(即使是弱表示性也能保证),而且当 F⊬A 时 F⊢¬B(┌A┐)。然而,用于证明第一不完备性定理的技术也表明,总是存在后者不成立的句子:可以构造相对于 B(x)对于 F 的哥德尔句子 GB。

(D)F⊢GB↔¬B(┌GB┐).

如前所述,可以得出 F⊬GB。假设 B(x)强表示定理集合,因此得出 F⊢¬B(┌GB┐),再根据(D),得出 F⊢GB,产生矛盾。因此,F 必须是不可判定的。

如果一个理论 F 的每个在 F 语言中的一致扩展都是不可判定的,则称 F 为本质上不可判定的。上述证明概述实际上证明了 Q 是本质上不可判定的。(有一些非常弱的理论是不可判定的,但不是本质上不可判定的。)

回想一下,Q 只有有限数量的公理,让 AQ 代表 Q 的公理的合取。那么对于算术语言中的任何句子 B,

当且仅当 AQ→B 是一阶逻辑的定理时,Q⊢B。

但是,一阶逻辑的决策过程将为 Q 提供一个决策方法。然而,后者是不可能的,因为已经被证明了。因此,可以得出结论:

** 哥德尔不完备定理** 一阶谓词逻辑是不可判定的。

(这个不可判定性结果最早由哥德尔在 1936 年 a、b 中建立;通过 Q 的不可判定性推导它的方法是由塔斯基、莫斯托夫斯基和罗宾逊在 1953 年提出的。)

随后,来自数学不同领域的许多理论和问题被证明是不可判定的(例如,参见 Davis 1977;Murawski 1999:第 3 章)。

4.3 反射原理和勒布定理

从启发性的角度来看,哥德尔句子 GF 可以被视为表达了自身的不可证明性——即“我是不可证明的”,尽管如前所述,这样的说法应该持保留态度。Leon Henkin 提出了一个问题,即表达自身可证明性的句子(“我是可证明的”)是真还是假,以及是否可证明(Henkin 1952)。Georg Kreisel 很快指出,这在很大程度上取决于可证明性的表达方式;不同的选择会得到相反的答案(Kreisel 1953)。

Martin Hugo Löb(1955)的论文,在一位评审的评论下,取得了在各个方面的重大进展。首先,它引入了现在标准的 Löb 可导性条件,这在之前的第二不完备性定理的背景下进行了讨论。其次,它包含了 Löb 对 Henkin 关于“表达自身可证性”的问题的解决方案。第三,它包含了一个现在称为“Löb 定理”的概括,但实际上 Löb 将其归功于匿名的评审人(恰好是 Henkin 本人;整个故事在 Smoryński 1991 中有详细叙述)。

为了正确理解 Löb 定理,首先有必要考虑所谓的“反射原理”。在上面的讨论中,重点是在形式系统内部表达系统的一致性,即 Cons(F)。但是,理论不仅应该是一致的,还应该是正确的,即只证明真实的句子。如何表达系统的正确性,即系统中可导出的一切都是真实的这一主张?如果想要用系统自身的语言来表达这一点,不能通过一个单一的陈述来实现,因为由于真理的不可定义性,在语言中没有合适的真理谓词可用。然而,可以通过一种方案来表达各种受限和不受限的正确性主张,这就是所谓的反射原理:

(Ref)ProvF(┌A┐)→A.

通过将 A 取为 ⊥,并注意到 ⊥ 在 F 中是可反驳的,很容易看出反射原理蕴含一致性陈述 Cons(F),即 ¬ProvF(┌⊥┐);因此它不能在系统中普遍可证。

这个方案也可以受限制。例如,等同于 1-一致性假设,或 Σ01-声音性,是将反射原理限制为 Σ01-句子(即方案中的句子 A 需要是 Σ01-句子)。或者,它可以限制为全局 Π01-句子;等等。

反射方案的哪些实例实际上可以在系统中被证明?Löb 定理对这个问题给出了精确的答案(假设 ProvF(x)满足可导性条件):

** 哥德尔不完备定理** 设 A 是 F 语言的任意句子。那么:如果且仅如果 F⊢ProvF(┌A┐)→A,那么 F⊢A。

因此,在一个系统中可证明的正确性实例(反射原理)正是那些涉及到在该系统中本身可证明的句子。作为结果,这也解决了亨金最初的问题:假设算术化的可证性谓词再次“正常”(即满足 Löb 的可导性条件),所有“断言自己可证性”的句子都是可证明的。

实际上,Löb 的定理可以很快地证明为第二不完备定理的结果。Kreisel 也指出,反过来,第二不完备定理也可以很容易地作为 Löb 的定理的结果推导出来。

4.4 Hilbert 的第十个问题和 MRDP 定理

Hilbert 在 1900 年的著名数学问题清单中的第十个问题要求找到一种决策方法来解决所谓的丢番图方程。尽管“丢番图”这个术语不常见,但这里讨论的是真正基础的问题。考虑任何一个涉及一个或多个变量、具有整数系数、只涉及加法和乘法的方程,例如 x2+y2=2 或 3x2+5y2+2xy=0。如果寻求实数解,通常只谈论“方程”。然而,在数论中,通常只寻求由整数组成的解。这是有很大区别的。上述方程中的前一个在实数中有无穷多个解,但在整数中只有四个解。方程 x2+y2=3 在实数中也有无穷多个解,但没有整数解。当关注的是整数解时,就谈论“丢番图方程”(以古代数论家亚历山大的丢番图斯命名)。

对于希尔伯特的第十个问题的一个正解,只需要提出一个具体的方法,该方法在直观上是一个“机械”的决策方法就足够了。然而,图灵对决策方法的概念进行的开创性分析引出了一个否定解的可能性。从 20 世纪 50 年代初开始,朱莉娅·罗宾逊和马丁·戴维斯开始研究这个问题,后来希拉里·普特南也加入了他们的研究。作为他们合作的结果,这个方向上的第一个重要结果被取得。如果一个方程涉及指数运算、加法和乘法(即指数可以是常数和变量),则称其为“指数丢番图方程”;自然地,重点仍然在于整数解。戴维斯、普特南和罗宾逊(1961 年)证明了指数丢番图方程的可解性问题是不可判定的。1970 年,尤里·马蒂亚塞维奇补充了最后缺失的部分,并证明了丢番图方程的可解性问题是不可判定的。因此,这个整体结果通常被称为 MRDP 定理(有关详细说明,请参见戴维斯 1973 年;马蒂亚塞维奇 1993 年)。

重要的技术成就是所有半可判定(可递归可枚举)集合都可以给出一个丢番图表示,即它们可以由形式为 ∃x1…∃xn(s=t)的简单公式表示,其中(s=t)是一个丢番图方程。更确切地说,对于任何给定的可递归可枚举集合 S,存在一个丢番图方程(s(y,x1,…,xn)=t(y,x1,…,xn)),使得当且仅当 n∈S 时,存在 x1…∃xn(s(n––,x1,…,xn)=t(n––,x1,…,xn))。

由于存在半可判定(可递归可枚举)集合而不可判定(递归)的情况,因此可以立即得出一般结论:

** MRDP 定理** 无法一般性地确定给定的丢番图方程是否有解。

这也提供了一个关于丢番图方程的优雅变体的不完备定理。

** 推论** 对于任何 1-一致的可公理化形式系统 F,存在着迪欧凡尼方程,它们没有解,但在 F 中无法证明它们没有解。

(在这里避免 1-一致性的要求是棘手的;参见 Dyson,Jones 和 Shepherson 1982 年。)

4.5 无法证明的陈述的具体案例

Gödel 的证明提供的不可判定句子(如果写出来)是非常复杂的公式,没有直观的意义,仅仅是为了不完备性证明的目的而构造的。然后就会产生一个问题,是否存在一些简单而自然的数学陈述,在选择的基本理论中同样是不可判定的,例如在 PA 中。现在已经有一些具有明确数学内容的特定陈述,在一些标准理论中已知是不可判定的(尽管这些陈述的自然性一直存在争议;参见 Feferman 1989b)。下面列举了一些众所周知的自然例子,从一些与 PA 无关的自然数学陈述开始,逐渐过渡到更强大的理论。有时这样的结果被称为 Gödel 定理的变体,或者它们的独立性证明被称为 Gödel 定理的替代证明,但这是误导性的:尽管它们可能很有趣,但它们没有 Gödel 定理本身的普遍性,只是提供了与特定理论无关的陈述。

据说在著名的巴黎-哈灵顿定理(见下文)之前,并没有人知道这样的自然独立数学陈述。然而,严格来说,这并不正确。早在 1935 年左右,Gerhard Gentzen(参见证明论发展条目)就提供了这样的陈述。将归纳的思想从自然数的领域推广到序数的领域是非常自然的。在集合论中,这样的推广被称为超限归纳原理。尽管一些构造主义者可能对完全集合论的合法性持怀疑态度,但在构造主义或直觉主义的观点下,有一些有限且更具体的超限归纳情况(仅涉及某些明确定义的可数序数类)是完全可接受的。一个重要的情况是超限归纳原理适用于被称为 ε0 的序数。Gentzen 证明了如果假设这个超限归纳原理,就可以证明 PA 的一致性。因此,由于第二不完备定理,这个原理本身在 PA 中是不能被证明的(Gentzen 1936)。

哥德尔不完备定理是在无穷组合学中的一个结果,由弗兰克·拉姆齐(1930 年)建立,并涉及对某些图形的“着色”可能性。杰夫·帕里斯和里奥·哈灵顿制定了拉姆齐定理的有限变体,并证明它在 PA 中是不可证明的(帕里斯和哈灵顿,1977 年)。这提供了一个相当自然的有限组合学陈述,它与 PA 无关。也许一个更清晰的例子是古德斯坦定理,由鲁本·古德斯坦(1944 年)提出,它纯粹是数论性质的。首先,我们定义了一类特定的自然数序列,现在称为“古德斯坦序列”。该定理表明,每个古德斯坦序列最终都会终止于 0。古德斯坦定理无疑是一个自然的数学陈述,因为它是由古德斯坦在很久以前(即 1944 年)通过证明方法(显然超出了 PA)提出和证明的,直到 1982 年才证明该定理在 PA 中是不可证明的(柯比和帕里斯,1982 年)。

现在转向超过 PA 的更强理论,例如,可以提到克鲁斯卡尔定理。这是一个涉及有限树的某种排序的定理(克鲁斯卡尔,1960 年)。哈维·弗里德曼证明了即使在比 PA 强得多的二阶算术子系统中,这个定理也是不可证明的(参见辛普森,1985 年)。特别是,在任何被预测合理化的理论中,它都是不可证明的(根据数学哲学条目中关于预测主义的部分的广泛接受的解释)。

在更强的理论中,甚至有一些数学命题是无法确定的具体例子,这些例子来自所谓的描述性集合论。这个数学领域与拓扑学有关,由法国半直觉主义者(勒贝格、贝尔、博雷尔等)发起(请参阅有关直觉主义的条目中关于描述性集合论的部分等)。它研究具有相对简单定义的集合(与半直觉主义者拒绝的任意集合和各种高阶幂集的概念相对立),这些集合被称为投射集或解析集。经典上,它们被定义为可以通过从可数个开集的交集中取连续映射和补集有限次得到的集合;它们与在 P2 语言中可定义的集合重合。特别地,所谓的博雷尔集合可以通过形如 ∃XA(x)和 ∀XB(x)的公式简单定义,其中 A 和 B 不包含任何集合变量(在逻辑学家的术语中,博雷尔集合是 Δ11 集合)。博雷尔函数的定义类似(请参阅,例如,Martin 1977)。

哈维·弗里德曼证明了以下定理:粗略地说,如果 S 是一个博雷尔集合,则存在一个博雷尔函数 f,使得 f 的图形要么包含在 S 中,要么与 S 不相交。弗里德曼证明了这个听起来很简单的定理甚至在完全的二阶算术 P2 中也无法证明,但证明它必然需要 ZFC 的全部力量(请参阅 Simpson 1999: 23)。

此外,这是描述性集合论的一个传统问题(可以用二阶算术的语言来表述),即所有投射集(见上文)是否都是勒贝格可测的。这个问题在很多年里一直是一个悬而未决的问题,而且有一个很好的理由:事实证明,这个陈述甚至与完整的 ZFC 集合论无关(见 Solovay 1970)。只有假设存在一些极大的基数(所谓的 Woodin 基数),才能证明所有投射集都是勒贝格可测的假设(这是 Woodin、Martin 和 Steel 在所谓的投射决策问题上的工作的结果;见 Woodin 1988;Martin 和 Steel 1988、1989)。

有时候,保罗·科恩(Paul Cohen)关于连续体假设(CH)与 ZFC 无关的著名结果(Cohen 1963, 1964;参见关于独立性和大基数的条目)。然而,这种情况非常不同。在上述所有独立性结果中,相关的陈述仍然是数学定理,被认为是真实的(最后一种情况需要超越 ZFC 的大基数公理,这更具有争议性;尽管如此,至少许多集合论学家认为这样的公理是可信的)。而且,在第一个不完备性定理本身中,只要系统的一致性假设是正确的,不可证明陈述的真实性就很容易得出。然而,在科恩的结果中,绝对没有任何迹象表明 CH 应该被认为是真实的、错误的,或者可能缺乏真值。

5. 哥德尔不完备定理的历史和早期接受情况

哥德尔的结果确实令人惊讶,但某种不完备现象并不完全出乎意料。1928 年,伯奈斯和塔斯基已经讨论了集合论背景下的不完备性可能性,而冯·诺伊曼与希尔伯特计划中的主导精神相反,认为逻辑和数学可能是不可判定的。哥德尔本人在他 1929 年的论文中提到了关于实数的一个不可判定问题的可能性(参见 Dawson 1985)。另一方面,希尔伯特(1928)假设皮亚诺算术和其他标准理论是完备的。显然,哥德尔也对布劳威尔印象深刻,布劳威尔在 1928 年的维也纳演讲中暗示数学是无穷的,无法完全形式化(参见 Wang 1987,84 页;以及关于直觉主义逻辑发展的条目中对布劳威尔对形式主义计划的看法的部分)。

无论如何,看起来哥德尔实际上是通过一条不同的途径得出了关于不完备性的第一个确切观察,这是在他试图为希尔伯特的计划做出贡献而不是破坏它的过程中(参见 Dawson 1997:第四章)。也就是说,在 1930 年,哥德尔努力推进希尔伯特的计划,试图证明分析(或者说二阶算术)与算术的资源一致,从而将前者的一致性归约到后者的一致性。在他的证明中,他需要真理的概念。哥德尔很快面临各种悖论(如说谎者悖论),不得不得出结论,算术真理无法在算术中定义。因此,哥德尔首先得出了一个关于真理不可定义性的版本,通常与塔斯基(Tarski)相关(参见 Murawski 1998)。这也很容易得出一个关于不完备性的弱版本:在算术中可证明的句子集可以在算术语言中定义,但真实的算术句子集却不能;因此两者不能重合。此外,在假设所有可证明的句子都是真的情况下,可以得出存在一些真句子是不可证明的。然而,这种方法并没有展示出任何特定的这样的句子。

然而,哥德尔所处的智力环境是维也纳学派,其具有根本反形而上学的态度。特别是,即使是真理的概念在当时也被认为是可疑的甚至是无意义的,至少在一些逻辑实证主义者(如诺伊拉特(Neurath)、亨普尔(Hempel))中是如此。因此,哥德尔努力消除对真理概念的任何诉求,并试图不使用它。因此,他引入了 ω-一致性的概念,这可以严格地、纯语法地定义。这导致了现在所知的不完备性定理的形式。

关于对角线引理,实际上哥德尔本人最初只证明了它的一个特殊情况,即仅针对可证性谓词。一般的引理显然是由卡尔纳普在 1934 年首次发现的(参见哥德尔 1934 年,1935 年)。对于带有自由变量的公式,还有更一般的版本,分别在 Ehrenfeucht&Feferman 1960 年和 Montague 1962 年提出(参见 Smoryński 1981 年)。

哥德尔的结果的接受程度是不一样的。一些逻辑学和数学基础领域的重要人物很快吸收了这些结果并理解了它们的相关性,但也存在着相当多的误解和抵制(有关接受情况的详细说明,请参见 Dawson 1985 年; Mancosu 1999 年)。

哥德尔于 1930 年 8 月 26 日在维也纳向卡尔纳普透露了他的研究结果,并在 1930 年 9 月 7 日著名的科尼斯堡会议上以一句随意的讨论中宣布了他的结果(第一个定理)。约翰·冯·诺伊曼当时在场,并且正在进行希尔伯特计划的研究,他立刻意识到这个结果的重要性。11 月 20 日,他给哥德尔写了一封信,介绍了他发现的哥德尔结果的一个“显著”推论:不可证明性(第二个定理)。与此同时,哥德尔自己也发现了同样的想法,并已经发送了他的文章的最终版本,其中还包括第二个不完备定理的陈述,以供出版。这篇文章于 1931 年 1 月出版(哥德尔 1931 年;关于哥德尔原始论文的有用介绍可参考 Kleene 1986 和 Zach 2005)。这些结果很快传播开来,显然对数学基础有重要意义,尽管对于真正的道义是什么,人们的观点不一。保罗·伯奈斯,希尔伯特最重要的合作者之一,对这些结果表现出极大的兴趣,尽管他最初在理解这些结果方面遇到了困难。他与哥德尔的积极通信也表明,哥德尔当时已经完全意识到真理的不可定义性。

由于哥德尔最初的方法集中在他的特定但非常全面的系统 P 及其(原始递归)扩展上,一些人对哥德尔的结果的普遍性表示怀疑。例如,阿隆佐·丘奇在 1932 年 7 月写给哥德尔的一封信中,建议哥德尔的结果不适用于他的 λ-转换系统(后来由克利尼和罗瑟证明该系统不一致)。哥德尔渴望推广他的发现,并在 1932 年和 1934 年的论文中将结果扩展到更广泛的系统类别。他还建议他的方法适用于标准的集合论系统(然而,直到几年后可判定性和丘奇-图灵论题的令人满意的特征化才能给出不完备定理的完全一般的表述(见上文);这首先是在克利尼 1936 年的论文中完成的)。著名的集合论学家恩斯特·策梅洛对哥德尔的工作提出了一些严厉的批评,但两人也就这个问题进行了通信。策梅洛似乎在理解相关概念和结果方面遇到了严重困难。

1933 年 3 月,哥德尔收到了来自苏黎世的保罗·芬斯勒的一封信,他认为他早在 1926 年(芬斯勒 1926 年)就已经做了与之密切相关但具有更广泛意义的工作。哥德尔回信称芬斯勒的系统根本没有被真正定义。在他激烈的回应中,芬斯勒声称,研究一个系统并不是必要的,它仍然可以被明确定义,并且他的想法与哥德尔的想法在原则上没有区别。回顾起来,芬斯勒和哥德尔的方法显然非常不同:对于哥德尔的工作,形式化系统的概念是至关重要的,而芬斯勒则拒绝了这个概念,认为它是人为限制的。事实上,芬斯勒的想法是否有任何意义还远未明确——无论它们与哥德尔的证明之间可能存在多么模糊的类比。

另一方面,可以说 Emil Post 在某些方面已经预见到了哥德尔的发现。他在 1922 年就已经得到了不完备性结果的抽象版本。特别是,他观察到他的方法将提供一个在《数学原理》中无法判定的陈述。然而,这些结果是基于 Post 自己对“丘奇-图灵论题”的版本,他对此不满意,并且他的工作没有发表。这些结果在(Post 1941)中被报道得更晚。

哥德尔定理的正确性在 1930 年代一直是一个激烈辩论的话题(参见 Dawson 1985)。1939 年,希尔伯特和伯奈斯的《数学基础》第二卷出版,其中详细证明了第二个不完备性定理。此后,在数理逻辑和数学基础领域积极工作的人中,对哥德尔的结论的严肃反对消失了。然而,在更多哲学领域,一些抵抗仍然存在。最著名的是,维特根斯坦在他的遗作《关于数学基础的注释》中对哥德尔的定理发表了一些批评性的言论。最初的主导反应是维特根斯坦根本没有理解这个结果。现在出现了更宽容的解释,这场辩论仍然非常活跃(参见维特根斯坦数学哲学条目中关于哥德尔和不可判定命题的部分)。

6. 哲学意义-真实和所谓的

6.1 数学哲学

在各个哲学领域中,哥德尔的定理显然与数学哲学最直接相关。首先,它们至少在表面上对希尔伯特的计划提出了严重的问题(这个问题在关于不完备性对希尔伯特计划影响的部分中有详细讨论)。然后,它们对直觉主义有重要的影响(参见数学哲学中关于直觉主义的条目)(另见哥德尔 1933 年,1941 年;Raatikainen 2005 年)。

关于哥德尔定理是否彻底驳斥逻辑主义存在争议(参见逻辑主义的条目)。例如,Henkin(1962 年)和 Musgrave(1977 年)认为它确实如此;Sternfeld(1976 年)和 Rodríguez-Consuegra(1993 年)持不同意见(另见 Hellman 1981 年;Raatikainen 2005 年)。

哥德尔本人根据不完备性定理(Gödel 1953/9)对逻辑实证主义的数学常规主义以及卡纳普的哲学观点提出了反驳。这一观点在 Goldfarb 和 Ricketts 1992 年、Ricketts 1995 年、Goldfarb 1995 年、Crocco 2003 年、Awodey&Carus 2003 年、2004 年以及 Tennant 2008 年的著作中进行了讨论。

6.2 自明和分析真理

人们还可以对哥德尔的定理给出更一般的认识论解释。例如,Quine 和 Ullian(1978)考虑了传统哲学观点,即所有真理都可以通过自明的步骤从自明的真理和观察中证明出来。然后他们指出,即使是基本数论的真理也不可能通过自明的步骤从自明的真理中推导出来(Quine&Ullian 1978: 64–65)。希拉里·普特南(Hilary Putnam)(1975)则认为,在某种自然理解下的“分析”中,根据哥德尔的定理,数学中必然存在合成真理。事实上,哥德尔本人也发表了非常类似的言论,即整数理论本身就是可证明的非分析的(Gödel 1944)。

6.3 “哥德尔式”反对机械论的论证

一直以来,人们一再尝试运用哥德尔的定理来证明人类思维的能力超越任何机械或形式系统。图灵在 20 世纪 40 年代末就考虑过这样一种反对机械论的哥德尔式论证(参见 Piccinini 2003),即使只是为了反驳它。在广为流传的通俗著作《哥德尔定理》中,纳格尔和纽曼(1958)从不完备定理中得出了一个毫无保留的反机械论结论。不久之后,卢卡斯(1961)声称哥德尔的不完备定理证明了机械论是错误的,也就是说,思维不能被解释为机器。

证明了机械论是错误的,也就是说,思维不能被解释为机器。

他声称

对于任何一台一致且能够进行简单算术运算的机器来说,存在一个它无法生成的被证明为真的公式...但我们可以看出它是真的。

最近,罗杰·彭罗斯(1989 年,1994 年)提出了非常类似的观点。约翰·西尔(1997 年)加入了讨论,并在某种程度上为彭罗斯辩护,反驳了他的批评者。克里斯平·赖特(1994 年,1995 年)从直觉主义的角度支持相关观点(有关批评,请参见 Detlefsen 1995)。他们都坚称哥德尔的定理意味着人类思维无限超越了任何有限的机器或形式系统的能力。

这些哥德尔反机械主义的论证是有问题的,广泛的共识是它们失败了。对这个论证的标准回应如下(这个反驳最早可以追溯到普特南 1960 年的论文;参见布洛斯 1968 年的论文,夏皮罗 1998 年的论文):这个论证假设对于任何形式化的系统或有限的机器,都存在一个在该系统中无法证明但人类思维可以看出是真实的哥德尔句子。然而,哥德尔的定理实际上是有条件的,一个系统的哥德尔句子的所谓真实性依赖于该系统一致性的假设。反机械主义的论证也要求人类思维总是能够看出一个给定的形式化理论是否一致。然而,这是非常不可信的(参见戴维斯 1990 年的论文)。卢卡斯、彭罗斯和其他人试图回应这样的批评(参见卢卡斯 1996 年的论文;彭罗斯 1995 年、1997 年的论文)。关于彭罗斯的详细批评,参见布洛斯 1990 年的论文;戴维斯 1990 年、1993 年的论文;费费尔曼 1995 年的论文;林德斯特伦 2001 年的论文;普德拉克 1999 年的论文;夏皮罗 2003 年的论文;这些考虑对卢卡斯的观点也是相关的)。

6.4 哥德尔和贝纳塞拉夫关于机械主义和形而上学的观点

有趣的是,哥德尔本人也提出了一个反机械主义的论证,尽管它更加谨慎,并且只在他的《哥德尔文集》第三卷(1995 年)中发表。也就是说,在他 1951 年的吉布斯讲座中,哥德尔从不完备定理中得出了以下的析取结论:

要么...人类思维(即使在纯数学领域内)无限超越任何有限机器的能力,要么存在绝对无法解决的丢番图方程问题。

哥德尔将这个陈述称为“数学上确立的事实”(哥德尔 1951 年;关于哥德尔的分离性主张的更多讨论,请参见 Shapiro 1998 年)。根据哥德尔的说法,第二种选择

似乎证明了数学只是我们自己创造的观点...数学对象和事实...客观存在并独立于我们的思维行为和决策。

哥德尔仍然倾向于否认绝对无解问题的可能性,尽管他确实相信数学上的普拉托主义,但他对这种信念的理由是不同的,他并没有坚持认为仅凭不完备定理就能建立普拉托主义。因此,哥德尔相信第一个分支,即人类思维无限超越任何有限机器的能力。然而,正如哥德尔自己明确解释的那样,哥德尔的这个结论只有在否认人类无法解决问题的可能性时才成立,正如哥德尔所做的那样。这不是不完备定理的必然结果。

与后来的所谓哥德尔反机械论论证的支持者不同,哥德尔足够敏感,承认机械论和人类绝对无解问题的替代方案与他的不完备定理是一致的。他不喜欢后者的根本原因更多是哲学上的。哥德尔以某种康德式的方式认为,如果人类理性提出无法回答的问题,那么它将变得致命的非理性(有关批判性讨论,请参见 Kreisel 1967;Boolos 1995;Raatikainen 2005)。

作为对卢卡斯论证的反应,但在哥德尔的吉布斯演讲发表之前,保罗·贝纳塞拉夫(1967)提出了更有资格的结论,有趣的是这些结论与哥德尔的一些思想相似。他认为,我确实是一个图灵机是与所有事实一致的,但我无法确定是哪一个。有关批判性讨论,请参见 Chihara 1972 和 Hanson 1971。

6.5 神秘主义和上帝的存在?

有时从哥德尔的定理中得出相当奇幻的结论。甚至有人认为,哥德尔的定理,如果不是确切地证明,至少对神秘主义或上帝的存在提供了强有力的支持。这些解释似乎假设了一个或多个已经在上面讨论过的误解:要么假设哥德尔提供了一个绝对无法证明的句子,要么假设哥德尔的定理意味着柏拉图主义,或反机械论,或两者兼而有之。

关于不完备定理的哲学方面的更多讨论,请参见 Raatikainen 2005 和 Franzén 2005。

Further reading

A standard reference for the incompleteness theorems is:

  • Smoryński, C., 1977, “The incompleteness theorems,” in Handbook of Mathematical Logic, J. Barwise (ed.), Amsterdam: North-Holland, pp. 821–866 [available online].

There are several introductory textbooks in mathematical logic which give a good exposition of the incompleteness theorems and related topics; for example:

  • Boolos, G., and R. Jeffrey, 1989, Computability and Logic, 3rd revised edition, Cambridge: Cambridge University Press.

  • Enderton, H., 1972, A Mathematical Introduction to Logic, New York: Academic Press.

  • Van Dalen, D., 2004, Logic and Structure, 4th edition, Berlin: Springer.

Two books that are dedicated to the incompleteness theorems are:

  • Smullyan, R., 1991, Gödel’s Incompleteness Theorems, Oxford: Oxford University Press.

  • Smith, P., 2007, An Introduction to Gödel’s Theorems, Cambridge: Cambridge University Press.

Another useful book on the incompleteness theorems and related topics is:

  • Murawski, R., 1999, Recursive Functions and Metamathematics: Problems of Completeness and Decidability, Gödel’s Theorems. Dordrecht: Kluwer.

A comprehensive, more advanced book on these themes is:

  • Hájek, P. and Pudlák, P., 1993, Metamathematics of First-Order Arithmetic, Berlin: Springer.

Another useful book, including also some more advanced topics is:

  • Franzén, T., 2004, Inexhaustibility: A Non-Exhaustive Treatment, Lecture Notes in Logic 16, ASL, Wellesley: A.K. Peters.

The more philosophical aspects around the incompleteness theorems are surveyed in the following two sources (Franzén is an accessible, informal, and yet reliable, explanation of the incompleteness theorems):

  • Raatikainen, P., 2005, “On the Philosophical Relevance of Gödel’s Incompleteness Theorems,” Revue Internationale de Philosophie, 59: 513–534 [available online].

  • Franzén, T., 2005, Gödel’s Theorem: An Incomplete Guide to its Use and Abuse, Wellesley: A.K. Peters.

The following two papers survey various issues around the first incompleteness theorem:

  • Beklemishev, L. D., 2010, “Gödel incompleteness theorems and the limits of their applicability. I,” Russian Mathematical Surveys, 65: 857–898.

  • Buldt, B., 2014, “The scope of Gödel’s first incompleteness theorem,” Logica Universalis, 8: 499–552.

Finally, there is an open-source e-book that contains a presentation of the incompleteness theorems:

Bibliography

  • Auerbach, David, 1985, “Intensionality and the Gödel theorems,” Philosophical Studies, 48 (3):337–51.

  • –––, 1992, “How to say things with formalisms,” in Proof, Logic, and Formalization, M. Detlefsen (ed.), London: Routledge, 77–93 [available online].

  • Awodey, S. & A.W. Carus, 2003, “Carnap versus Gödel on Syntax and Tolerance,” in Logical Empiricism: Historical and Contemporary Perspectives, P. Parrini et al. (eds.), Pittsburgh: University of Pittsburgh Press, pp. 57–64 [available online].

  • –––, 2004, “How Carnap Could Have Replied to Gödel,” in S. Awodey and C. Klein (eds.), Carnap Brought Home: The View from Jena, LaSalle, IL: Open Court, pp. 203–223 [available online].

  • Barzin, M., 1940, “Sur la portée du théorème de M. Gödel,” Académie Royale de Belgique, Bulletin de la Classe des Sciences, Series 5, 26: 230–39.

  • Benacerraf, P., 1967, “God, the Devil, and Gödel,” The Monist, 51: 9–32 [available online].

  • Bezboruah, A. and J.C. Shepherdson, 1976, “Gödel’s Second Incompleteness Theorem for Q,” The Journal of Symbolic Logic, 41: 503–512.

  • Boolos, G., 1968, “Review of ‘Minds, Machines and Gödel’, by J.R. Lucas, and ‘God, the Devil, and Gödel’,” Journal of Symbolic Logic, 33: 613–15.

  • –––, 1990, “On ‘Seeing’ the Truth of Gödel Sentence,” Behavioral and Brain Sciences, 13: 655–656.

  • –––, 1995, “Introductory Note to *1951,” in Gödel 1995: 290–304.

  • Boolos, G. and R. Jeffrey, 1989, Computability and logic, 3rd revised edition, Cambridge: Cambridge University Press.

  • Carnap, R., 1934, Logische Syntax der Sprache, Vienna: Julius Springer.

  • Chihara, C., 1972, “On Alleged Refutations of Mechanism Using Gödel’s Incompleteness Results,” Journal of Philosophy, 69: 507–26.

  • Church, A., 1936a, “An Unsolvable Problem of Elementary Number Theory,” American Journal of Mathematics, 58: 354–363. Republished in Davis 1965, 89–107.

  • –––, 1936b, “A Note on Entscheidungsproblem,” Journal of Symbolic Logic, 1: 40–41; correction, ibid., 101–102. Republished in Davis 1965, 110–115.

  • Cohen, P. J., 1963, “The Independence of the Continuum Hypothesis I,” Proceedings of the National Academy of Sciences, (U.S.A.), 50(6): 1143–48.

  • –––, 1964, “The Independence of the Continuum Hypothesis II,” Proceedings of the National Academy of Sciences, (U.S.A.), 51(1): 105–110.

  • Crocco, G., 2003, “Gödel, Carnap, and the Fregean Heritage,” Synthese, 137: 21–41.

  • Davis, M., 1965, The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions, Hewlett, NY: Raven Press.

  • –––, 1973, “Hilbert’s Tenth Problem is Unsolvable,” The American Mathematical Monthly, 80: 233–269.

  • –––, 1977, “Unsolvable Problems,” in Handbook of Mathematical Logic, J. Barwise (ed.), Amsterdam: North-Holland, pp. 567–594.

  • –––, 1990, “Is Mathematical Insight Algorithmic?” Behavioral and Brain Sciences, 13: 659–660.

  • –––, 1993, “How Subtle is Gödel’s Theorem? More on Roger Penrose,” Behavioral and Brain Sciences, 16: 611–612.

  • Davis, M., H. Putnam, and J. Robinson, 1961, “The decision problem for exponential diophantine equations,” Annals of Mathematics (2), 74(3): 425–436.

  • Dawson, J., 1985, “The Reception of Gödel’s Incompleteness Theorems,” PSA: Proceedings of the Biennial Meeting of the Philosophy of Science Association 1984, vol. II, pp. 253–271.

  • –––, 1997, Logical Dilemmas: The Life and Work of Kurt Gödel, Natick, MA: A. K. Peters.

  • Detlefsen, M., 1979, “On Interpreting Gödel’s Second Theorem,” Journal of Philosophical Logic, 8(1): 297–313.

  • –––, 1986, Hilbert’s Program: An Essay in Mathematical Instrumentalism, Dordrecht: Reidel.

  • –––, 1990, “On an Alleged Refutation of Hilbert’s Program Using Gödel’s First Incompleteness Theorem,” Journal of Philosophical Logic, 19(4): 343–377.

  • –––, 1995, “Wright on the Non-mechanizability of Intuitionist Reasoning,” Philosophia Mathematica, 3(1): 103–118.

  • –––, 2001, “What Does Gödel’s Second Theorem Say?” Philosophia Mathematica, 9: 37–71.

  • Dyson, V., J.P. Jones, and J.C. Shepherdson, 1982, “Some Diophantine Forms of Gödel’s Theorem,” Archiv für Mathematische Logik und Grundlagenforschung, 22: 51–60.

  • Ehrenfeucht, A. and S. Feferman, 1960, “Representability of recursively enumerable sets in formal theories”, Arch. Math. Logik Grundlag., 5(1–2), 37–41.

  • Feferman, S., 1960, “Arithmetization of Metamathematics in a General Setting,” Fundamenta Mathematicae, 49: 35–92.

  • –––, 1982, “Inductively Presented Systems and the Formalization of Meta-mathematics,” in Logic Colloquium ’80, D. van Dalen et al. (eds.), Amsterdam: North-Holland, pp. 95–128.

  • –––, 1989a, “Finitary Inductively Presented Logics,” in Logic Colloquium ‘88, R. Ferro, et al. (eds.), Amsterdam: North-Holland, pp. 191–220. [available online]

  • –––, 1989b, “Infinity in Mathematics: Is Cantor Necessary?” Philosophical Topics, 17(2): 23–45.

  • –––, 1995, “Penrose’s Gödelian argument: A Review of Shadows of Mind, by Roger Penrose,” Psyche, 2 (7).

  • –––, 1997, “My Route to Arithmetization,” Theoria, 63: 168–181.

  • Finsler, P., 1926, “Formale Beweise und die Entscheidbarkeit,” Mathematische Zeitschrift, 25: 676–82.

  • Fitting, M., 2007, Incompleteness in the land of sets, London: College Publications. Series: Studies in logic ; v. 5.

  • Franks, C., 2009, The Autonomy of Mathematical Knowledge. Hilbert’s Program Revisited, Oxford: Oxford University Press.

  • Gaifman, H., 2006, “Naming and Diagonalization, From Cantor to Gödel to Kleene,” Logic Journal of the IGPL, 14: 709–728. [available online]

  • Gentzen, G., 1936, “Die Widerspruchsfreiheit der reinen Zahlentheorie,” Mathematische Annalen, 112: 493–565.

  • Gödel, K., 1931, “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I,” Monatshefte für Mathematik Physik, 38: 173–198. English translation in van Heijenoort 1967, 596–616, and in Gödel 1986, 144–195.

  • –––, 1932, “Über Vollständigkeit und Widerspruchsfreiheit,” Ergebnisse eines mathematischen Kolloquiums, 3: 12–13. English translation “On Completeness and Consistency” in Gödel 1986: 235–7.

  • –––, 1933, “The Present Situation in Foundations of Mathematics,” in Gödel 1995: 45–53.

  • –––, 1934, “On Undecidable Propositions of Formal Mathematical Systems” (mimeographed lecture notes; taken by S. Kleene and J. Rosser), reprinted with corrections in Davis 1965, 41–81, and Gödel 1986, 346–371.

  • –––, 1935, “Review of Carnap 1934,” in Gödel 1986: 389.

  • –––, 1941, “In What Sense is Intuitionistic Logic Constructive?” in Gödel 1995: 189–200.

  • –––, 1944, “Russell’s Mathematical Logic,” in The Philosophy of Bertrand Russell, P. A. Schilpp (ed.), Evanston, Il.: Northwestern University, pp. 125–153. Reprinted in Gödel 1990: 119­–141.

  • –––, 1951, “Some Basic Theorems on the Foundations of Mathematics and their Implications” (Gibbs Lecture), in Gödel 1995: 304­–323.

  • –––, 1953/9, “Is Mathematics a Syntax of Language?,” lecture manuscript (two versions), in Gödel 1995: 334–362.

  • –––, 1963, “Note added 28 August 1963” (to Gödel 1931), in Gödel 1986: 195.

  • –––, 1986, Collected Works I. Publications 1929–1936, S. Feferman et al. (eds.), Oxford: Oxford University Press.

  • –––, 1990, Collected Works II. Publications 1938–1974, S. Feferman et al. (eds.), Oxford: Oxford University Press.

  • –––, 1995, Collected Works III. Unpublished Essays and Lectures, S. Feferman et al. (eds.), Oxford: Oxford University Press.

  • Goldfarb, W., 1995, “Introductory Note to *1953/9,” in Gödel 1995: 324–334.

  • Goldfarb, W. and T. Ricketts, 1992, “Carnap and the Philosophy of Mathematics,” in Science and Subjectivity, D. Bell and W. Vossenkuhl (eds.), Berlin: Akademie Verlag, pp. 61–78.

  • Gómez Torrente, M., 2004, “The Indefinability of Truth in the Wahrheitsbegriff,” Annals of Pure and Applied Logic, 126(1–3): 27–37. [available online]

  • Goodstein, R., 1944, “On the Restricted Ordinal Theorem,” The Journal of Symbolic Logic, 9: 33–41.

  • Grelling, K., 1937, “Gibt es eine Gödelsche Antinomie?,” Theoria, 3: 297–306.

  • Hanson, W.H., 1971, “Mechanism and Gödel’s theorems,” The British Journal for the Philosophy of Science, 22: 9–16.

  • Hellman, G., 1981, “How to Gödel a Frege-Russell: Gödel’s Incompleteness Theorems and Logicism,” Nous, 15: 451–468.

  • Helmer, O., 1938, “Perelman versus Gödel,” Mind, 46: 58–60.

  • Henkin, L., 1952, “Problem,” The Journal of Symbolic Logic, 17: 160.

  • –––, 1962, “Are Mathematics and Logic Identical?” Science, 138: 788–794.

  • Hilbert, D., 1928, “Die Grundlagen der Mathematik,” Abhandlungen aus dem Mathematischen Seminar der Hamburgischen Universität, 6: 65–85. English translation in van Heijenoort 1967.

  • Hilbert, D. and P. Bernays, 1939, Grundlagen der Mathematik, vol. 2, Berlin: Springer.

  • Jeroslow, R., 1973, “Redundancies in the Hilbert-Bernays Derivability Conditions for Gödel’s Second Incompleteness Theorem,” Journal of Symbolic Logic, 38: 359–367.

  • Kaye, R., 1991, Models of Peano Arithmetic, (Oxford Logic Guides), Oxford: Clarendon Press.

  • Kirby, L. and J. Paris, 1982, “Accessible Independence Results for Peano Arithmetic,” Bull. London. Math. Soc., 14: 285–93.

  • Kleene, S.C., 1936, “General recursive functions of natural numbers,”, Mathematische Annalen 112(1): 727–742.

  • –––,1937a, “Review of Perelman 1936,” Journal of Symbolic Logic, 2: 40–41.

  • –––, 1937b, “Review of Helmer 1937,” Journal of Symbolic Logic, 2: 48–49.

  • –––, 1986, “Introductory note to 1930b, 1931 and 1932b”, in Gödel 1986, pp. 126–141.

  • Kreisel, G., 1953, “On a Problem of Henkin’s,” Proc. Netherlands Acad. Sci. 56: 405–406.

  • –––, 1958, “Mathematical significance of consistency proofs,” The Journal of Symbolic Logic, 23: 159–182.

  • –––, 1967, “Mathematical Logic: What Has it Done For the Philosophy of Mathematics?” in Bertrand Russell: Philosopher of the Century, R. Schoenman (ed.), London: George Allen and Unwin.

  • Kruskal, J.B., 1960, “Well-quasi-ordering, the Tree Theorem, and Vazsonyi’s Conjecture,” Transactions of the American Mathematical Society, 95 (2): 210–225.

  • Lindström, P., 2001, “Penrose’s New Argument,” Journal of Philosophical Logic, 30(3): 241–250.

  • Lucas, J. R., 1961, “Minds, Machines, and Gödel,” Philosophy, 36(137): 112–137 [available online].

  • –––, 1996, “Minds, Machines, and Gödel: A Retrospect,” in Machines and Thought. The Legacy of Alan Turing, Vol. 1, P.J.R. Millican and A. Clark (eds.), Oxford: Oxford University Press, 103–124.

  • Löb, M. H., 1955, “Solution of a Problem of Leon Henkin,” Journal of Symbolic Logic, 20: 115–118.

  • Mancosu, P., 1999, “Between Vienna and Berlin: The Immediate Reception of Gödel’s Incompleteness Theorems,” History and Philosophy of Logic, 20: 33–45.

  • Martin, D., 1977, “Descriptive Set Theory: Projective Sets,” in Handbook of Mathematical Logic, J. Barwise (ed.), Amsterdam: North-Holland, 783–815.

  • Martin, D. and Steel, J., 1988, “Projective Determinacy,” Proceedings of the National Academy of Sciences, (U.S.A.), 85: 6582–86.

  • –––, 1989, “A Proof of Projective Determinacy,” Journal of the A.M.S., 2: 71–125.

  • Matiyasevich, Y., 1970, “Diofantovost’ perechislimykh mnozhestv,” Dokl. Akad. Nauk SSSR, 191(2): 297–282 (Russian). (English translation, 1970, “Enumerable sets are Diophantine,” Soviet Math. Dokl., 11(2): 354–358.)

  • –––, 1993, Hilbert’s Tenth Problem, Cambridge, MA: MIT Press.

  • Milne, P., 2007, “On Gödel Sentences and What They Say,” Philosophia Mathematica, 15: 193–226.

  • Montague, R., 1962, “Theories Incomparable with Respect to Relative Interpretability,” The Journal of Symbolic Logic, 27: 195–211.

  • Murawski, R., 1998, “Undefinability of Truth. The Problem of Priority: Tarski vs. Gödel,” History and Philosophy of Logic, 19: 153–160.

  • –––, 1999, Recursive Functions and Metamathematics: Problems of Completeness and Decidability, Gödel’s Theorems, Dordrecht: Kluwer.

  • Musgrave, A., 1977, “Logicism Revisited,” British Journal for the Philosophy of Science, 28: 99–127.

  • Nagel, E. and J.R. Newman, 1958, Gödel’s Proof, New York: New York University Press.

  • Paris, J. and L. Harrington, 1977, “A Mathematical Incompleteness in Peano Arithmetic,” in Handbook of Mathematical Logic, J. Barwise (ed.), Amsterdam: North-Holland, pp. 1133–1142 [available online].

  • Paris, J. and L. Kirby, 1978, “Sn Collection Schema in Arithmetic,” in Logic Colloquium ’77, A. McIntyre et al. (eds.), Amsterdam: North-Holland, pp. 199–209.

  • Parsons, C., 1970, “On Number Choice Schema and its Relation to Induction,” in Intuitionism and Proof Theory, Kino et al. (eds.), Amsterdam: North-Holland, pp. 459–473.

  • Penrose, R., 1989, The Emperor’s New Mind: Concerning Computers, Minds, and the Laws of Physics, New York: Oxford University Press.

  • –––, 1994, Shadows of the Mind: A Search for the Missing Science of Consciousness, New York: Oxford University Press

  • –––, 1995, “Beyond the Doubting of a Shadow: A Reply to Commentaries of Shadows of the Mind,” Psyche, Vol 2.

  • –––, 1997, “On understanding understanding”, International Studies in the Philosophy of Science, 11: 7–20.

  • Perelman, C., 1936, “L’Antinomie de M. Gödel,” Académie Royale de Belgique. Bulletin de la Classe des Sciences (Series 5), 22: 730–36.

  • Piccinini, G., 2003, “Alan Turing and the Mathematical Objection,” Minds and Machines, 13: 23–48.

  • Post, E., 1941, “Absolutely Unsolvable Problems and Relatively Unsolvable Propositions: Account of an Anticipation,” published in Davis 1965, 338–433.

  • Presburger, M., 1929, “Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt,” Sprawozdanie z I Kongresu Matematyków Krajów Slowiańskich, (= Comptes-rendus du I Congrès Mathématiciens des Pays Slaves), Warsaw, pp. 92–101. English translation, 1991,“On the completeness of a certain system of arithmetic of whole numbers in which addition occurs as the only operation,” History and Philosophy of Logic, 12(2): 225–232.

  • Pudlák, P., 1996, “On the Length of Proofs of Consistency,” Collegium Logicum, Annals of the Kurt-Gödel-Society, 2: 65–86.

  • –––, 1999, “A Note on Applicability of the Incompleteness Theorem to Human Mind,” Annals of Pure and Applied Logic, 96: 335–342.

  • Putnam, H., 1960, “Minds and machines,” in Dimensions of Mind, S. Hook (ed.), New York: New York University Press. Reprinted in H. Putnam, 1975, Mind, Language, and Reality. Philosophical Papers, Vol 2, Cambridge: Cambridge University Press, pp. 325–341.

  • –––, 1975, “What is Mathematical Truth?” Historia Mathematica, 2: 529–545. Reprinted in H. Putnam, 1975, Mathematics, Matter and Method. Philosophical Papers, Vol 1, Cambridge: Cambridge University Press, pp. 60–78.

  • Quine, W.V. and J.S. Ullian, 1978, The Web of Belief, 2nd ed., New York: Random House.

  • Raatikainen, P., 2005, “On the Philosophical Relevance of Gödel’s Incompleteness Theorems,” Revue Internationale de Philosophie, 59: 513–534.

  • Ramsey, F. P., 1930, “On a Problem of Formal Logic,” Proceedings of the London Mathematical Society, series 2, 30: 264–286.

  • Ricketts, T., 1995, “Carnap’s Principle of Tolerance, Empiricism, and Conventionalism,” in Reading Putnam, P. Clark & B. Hale (eds.), Cambridge: Blackwell, pp. 176–200.

  • Rodríguez-Consuegra, F., 1993, “Russell, Gödel and Logicism,” in Philosophy of Mathematics, J. Czermak (ed.), Vienna: Hölder-Pichler-Tempsky, pp. 233–42. Reprinted in, 1998, Bertrand Russell: Critical Assessments, A. Irvine (ed.), vol. 2: Logic and mathematics, London: Routledge, pp. 320–29.

  • Roeper, P., 2003, “Giving an Account of Provability within a Theory,” Philosophia Mathematica, 11: 332–340.

  • Rosser, J. B., 1936, “Extensions of Some Theorems of Gödel and Church,” Journal of Symbolic Logic, 1: 87–91.

  • –––, 1938, “Review: Kurt Grelling, Gibt es eine Godelsche Antinomie? [Grelling 1937/8],” Journal of Symbolic Logic, 3(2): 86.

  • Searle, J., 1997, “Roger Penrose, Kurt Gödel, and the Cytoskeletons,” in J. Searle: Mystery of Consciousness, New York: New York Review of Books, pp. 55–93.

  • Shapiro, S., 1998, “Incompleteness, Mechanism, and Optimism,” Bulletin of Symbolic Logic, 4: 273–302.

  • –––, 2003, “Mechanism, Truth and Penrose’s New Argument,” Journal of Philosophical Logic, 32(1): 19–42.

  • Simpson, S.G., 1985, “Nonprovability of Certain Combinatorial Properties of Finite Trees,” in Harvey Friedman’s Research on the Foundations of Mathematics, L. Harrington et al. (eds.), Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland, pp. 87–117

  • –––, 1999, Subsystems of Second Order Arithmetic, Berlin: Springer.

  • Skolem, T., 1930, “Über einige Satzfunktionen in der Arithmetik,” Skrifter utgitt av Det Norske Videnskaps-Akademi i Oslo, I, no. 7, 1–28. Reprinted in T. Skolem, 1970, Selected Works in Logic, (J. Fenstad, editor), Oslo: Universitetsforlaget, pp. 281–306.

  • Smoryński, C., 1977, “The Incompleteness Theorems,” in Handbook of Mathematical Logic, J. Barwise (ed.), Amsterdam: North-Holland, pp. 821–865.

  • –––, 1981, “Fifty Years of Self-reference in Arithmetic,” Notre Dame Journal of Formal Logic, 22(4): 357–374.

  • –––, 1991, “The Development of Self-reference: Löb’s Theorem,” in Perspectives on the History of Mathematical Logic, T. Drucker (ed.), Birkhauser, pp. 111–133.

  • Smullyan, R., 1992, Gödel’s Incompleteness Theorems, Oxford: Oxford University Press.

  • Solovay, R.M., 1970, “A Model of Set Theory in which Every Set of Reals is Lebesgue Measurable,” Annals of Mathematics, 92: 1–56.

  • Sternfeld, R., 1976, “The Logistic Thesis,” in Studien zu Frege/Studies on Frege I, M. Schirn (ed.), Stuttgart-Bad Cannstatt: Frommann-Holzboog, pp. 139–160.

  • Tarski, A., 1948, A Decision Method for Elementary Algebra and Geometry, manuscript. Santa Monica, CA: RAND Corp., 1948. Republished as A Decision Method for Elementary Algebra and Geometry, 2nd ed. Berkeley, CA: University of California Press, 1951.

  • Tarski, A., A. Mostowski, and R.M. Robinson, 1953, Undecidable Theories, Amsterdam: North-Holland.

  • Tennant, Neil, 2008, “Carnap, Gödel, and the Analyticity of Arithmetic”, Philosophia Mathematica, 16: 100–112.

  • Turing, A.M., 1936–7, “On Computable Numbers, with an Application to the Entscheidungsproblem,” Proceedings of the London Mathematical Society, Series 2, 42: 230–265; correction, ibid., 43: 544–546. Republished in Davis 1965, 115–154.

  • Van Heijenoort, J. (ed.), 1967, From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931, Cambridge, MA: Harvard University Press.

  • Visser, A., 2011, “Can We Make the Second Incompleteness Theorem Coordinate Free,” Journal on Logic and Computation, 21(4): 543–560.

  • Woodin, H., 1988, “Supercompact Cardinals, Sets of Reals, and Weakly Homogeneous Trees,” Proceedings of the National Academy of Sciences, (U.S.A.), 85: 6587–91.

  • Wright, C., 1994, “About ‘The Philosophical Significance of Gödel’s Theorem’: Some Issues,” in The Philosophy of Michael Dummett, B. McGuinness and G. Oliveri (eds.) Dordrecht: Kluwer, pp. 167–202.

  • –––, 1995, “Intuitionists are not (Turing) Machines,” Philosophia Mathematica, 3: 86–102.

  • Zach, R., 2005, “Paper on the Incompleteness Theorems,” in Landmark Writings in Western Mathematics, I. Grattan-Guinness (ed.), Amsterdam: Elsevier, pp. 917–25 [available online].

Academic Tools

Other Internet Resources

Church-Turing Thesis | Gödel, Kurt | Hilbert, David: program in the foundations of mathematics | logic, history of: intuitionistic logic | logic: second-order and higher-order | mathematics, philosophy of | mathematics, philosophy of: intuitionism | proof theory | proof theory: development of | recursive functions | set theory | set theory: independence and large cardinals | Turing machines | Wittgenstein, Ludwig: philosophy of mathematics

Acknowledgments

The author would like to thank Richard Zach for his careful and valuable comments on the earlier drafts of this entry. The author and SEP editors would like to thank Richard O’Callaghan for bringing to our attention that, in an earlier version of the supplement on the Diagonalization Lemma, the definition of the substitution function, although standard, didn’t suffice for the purposes of the proof.

Copyright © 2020 by Panu Raatikainen <panu.raatikainen@tuni.fi>

最后更新于

Logo

道长哲学研讨会 2024