阿朗佐教堂

阿朗佐·丘奇（Alonzo Church，1903-1995）是一位著名的数理逻辑学家、哲学逻辑学家、哲学家、教师和编辑。他是继康托、弗雷格和罗素之后数理逻辑学科的创始人之一。他也是符号逻辑协会和符号逻辑杂志的主要创始人之一。他的数学和哲学学生名单引人注目，因为其中包含著名逻辑学家和哲学家的名字。在本文中，我们主要关注丘奇的哲学贡献。 （有关他的生平和学术史的叙述，请参阅《阿隆佐·丘奇文集简介》（2019 年）。）但是，当为了追求哲学问题而需要这样做时，我们也会讨论他的数学结果。在丘奇的例子中，哲学家和形式逻辑学家/数学家之间的区别并不完全正确，因为他的所有工作（除了偶尔关于某些纯数学主题的论文）都以这样或那样的方式关注逻辑问题。

丘奇通过将他的“逻辑方法”应用于他所讨论的哲学主题，以一种独特的方式将形式逻辑的总体观点和具体区别引入哲学。相反，他还将他的哲学的某些方面融入到他所提出的形式数学逻辑的结构中。结果是哲学视野和集中论证的强大结合。对于丘奇来说，逻辑方法（或形式化）不仅对于获得非正式讨论之外的额外澄清以及使元数学研究成为可能是必要的；它也是处理认识论、形而上学和语言哲学等哲学问题的理想方法。丘奇认为，不追求这一理想的人就达不到目标。然而，他也认识到形式化并不总是合适的。他并不要求自然科学形式化，甚至在他的《数理逻辑导论》（1956a）的介绍性章节中提供了对语义的非正式哲学讨论。本文讨论的理论和论点描述并说明了丘奇的逻辑学方法。

在下文中，我们经常使用 Church 从《数学原理》（Whitehead & Russell 1910；以下简称 PM）中采用的符号约定。当我们这样做时，这些约定会得到解释，有时还会与现代符号进行比较。

1. 可计算性和 Church 的论文

1.1 Church 的开创性论文

1.2 什么是教会论文？

1.3 CT1的作用

1.4 外部证据

1.5 内部证据

2.逻辑哲学

2.1 逻辑哲学和Logistic方法

2.2 采用形式化语言

2.3 逻辑与沟通

3.Logistic方法的应用

3.1 反对逻辑经验主义

3.2 弹弓论证

3.3 翻译论证

3.4 分析的悖论

3.5 意义与外延的逻辑

4. 悖论

4.1 教会工作中的矛盾

4.2 格雷林悖论

4.3 比较拉塞尔和塔斯基

4.4 GP的推导与消解

4.5 拉塞尔-迈希尔悖论

4.6 可知性悖论

5. 数学基础

5.1 无类型基础的尝试

5.2 类型论与集合论基础

5.3 逻辑主义和直觉主义

5.4.哥德尔定理和连续统问题的意义

6.形而上学

6.1 形而上学和逻辑方法

6.2 教会的谦虚现实主义

6.3 关于命题的现实主义

参考书目

主要来源

二手资料

学术工具

其他互联网资源

相关条目

补充剂清单

A. Church on Computability（§1）

B. 早期逻辑哲学和形而上学（§2）

C. Logistic 方法的应用（第 3 节）

D. λ 演算和类型理论（适用于 §§3、4、5）

E. 语言哲学（§§3、4）

F. 悖论以及与 Tarski 的比较（§4）

1. 可计算性和 Church 的论文

1.1 Church 的开创性论文

Church 是第一个设计出一种形式主义（λ 演算）的人，在这种形式主义中，可以定义一类函数，这些函数可以说与直观可计算的函数（可以通过算法（即计算机程序）进行评估的函数）一致。他还提供了第一个不可计算的特定重要函数的例子，这也是有争议的。 （其他独立于 Kleene (1936) 和 Turing (1936) 的例子也很快跟进。）他通过构造一个可证明不是哥德尔和赫布兰德稍早定义的意义上的递归函数来做到这一点。然后，他利用任何直观可计算函数都是递归的假设来得出结论：所讨论的函数是不可计算的——用丘奇的术语来说，它不是有效可计算的。 （我们将继续使用术语“可计算”和“直观可计算”，而不是“有效可计算”，因为它们更容易被非专业人士理解。）考虑到这个函数的性质，这意味着初等数论的某个问题是无法解决的：无法通过算法手段解决它。它还暗示了对 Hilbert 和 Ackerman (1928) 首次阐明的 Entscheidungsproblem 的否定解决方案：一阶逻辑是否存在决策过程的问题。这个斜体假设后来被称为“丘奇论文”（Kleene 1952）。

提出这一结果的论文题为“基本数论不可解的问题”（1936a），是逻辑和可计算性理论的伟大经典，但它在某种程度上被图灵（1936）几乎同时代的辉煌论文以及哥德尔（1931）早期引人注目的不完备性定理所掩盖。在本节中，丘奇的论文占据了中心舞台。

Church 论文的第 7 节包含了 Church 论文的第一个明确表述（除了 1935c 的初步陈述之外）：

我们现在通过将正整数的递归函数（或正整数的 lambda 可定义函数）的概念识别出来来定义已经讨论过的正整数的有效可计算函数的概念。只要能够为选择与直观概念相对应的正式定义获得积极的理由，就可以认为该定义是通过以下考虑来证明的。 （1936a [BE：119]）

Church 继续考虑两种自然的方式，人们可能会寻求将可计算性的概念扩展到递归性（或 λ 可定义性）之外，他认为这些方法中的每一种都会产生已经递归的（和 λ 可定义的）函数，因此得出结论：

因此，结果表明，通过两种方法中的任何一种都无法获得比上面提出的更一般的有效可计算性定义，这两种方法自然表明它们自己（1）如果存在计算其值的算法，则通过定义可有效计算的函数（2）如果对于每个正整数m，存在一个正整数n，使得F（m）= n是可证明定理，则通过定义可有效计算的函数F（一个正整数）。 （1936a [BE：121]）

Kleene（1952：222-223）讨论了丘奇论文的这两个经典论点。 （更多详情请参见补充 A.2。）

1.2 什么是教会论文？

丘奇的论文是以下两个命题中的第一个，但第二个命题在第一个命题的讨论中起着重要作用。我们使用术语“CT”来表示两者的结合：

CT1

每个直观可计算的函数都是递归的

CT2

每个递归函数都是直观可计算的。

CT 可以根据 λ 可定义性或图灵可计算性或已知可扩展等价于递归性的许多其他不同数学条件来表述。尽管存在这些相同之处，但差异仍然很大。哥德尔曾多次表达了对图灵分析的强烈偏爱，而且哥德尔的偏爱是有充分理由的。这些在其他地方有详细的说明（参见 Church-Turing 论文以及 Davis 1965 的条目）。丘奇本人认为图灵的分析优于他的：

图灵机的可计算性……具有使普通（未明确定义）意义上的有效性识别立即显而易见的优点。 （教堂 1937a [BE: 934]）

λ-可定义性与直观可计算性的识别当然不是“立即显而易见”的。事实上，Church 的学生 Stephen Cole Kleene 报告说，Church、Rosser（J. Barkley Rosser，也是 Church 的学生）和他自己才逐渐意识到 λ 可定义性可以作为直觉可计算性的精确对应物（Kleene 1981）。 Kleene 还描述了给出某些基本数论函数（尤其是前驱函数）的 λ 定义的困难，因为 Church 给出了代表整数的 λ 表达式（1981：56；这些 λ 表达式在补充 D 中描述）。但正如 Church (1936a) 所阐明的那样，CT1 的根本困难在于它是作为一个定义给出的，除了 λ 可定义性和递归性的外延等价性证明的简要草图之外，没有任何附带的论证（Kleene [1936] 给出了更详细的证明）。哥德尔正是抱怨这一点：

他[哥德尔]坚持认为，如果不首先表明有效可计算性概念的“普遍接受的属性”必然导致该类，那么将有效可计算函数定义为某个特定类是“完全不能令人满意”的。 （戴维斯1982：12）

哥德尔最终将图灵的分析视为更好的计算模型，正是因为图灵在详细分析配备纸和铅笔的人类计算机实际上必须做什么的基础上证明了直观计算与图灵机计算的一致性（Turing 1936：§9）。对于 λ 计算的情况，似乎还没有给出图灵令人信服的分析的对应部分。然而，应该强调的是，丘奇的主要目的不是捍卫可计算性分析，而是为证明特定数论组合问题不可解决奠定基础。只要计算被定义为有限过程，基数考虑就意味着必须存在不可计算的函数，而丘奇希望证明他的组合问题就是其中之一。

在其生命的大部分时间里，Church 的观点——CT1 不受数学证明或任何形式的数学处理——一直盛行。但一些人，如 Shoenfield（以及 Church 本人），观察到 CT2 受到直观证明的影响，尽管缺乏“可计算”的数学精确定义（Shoenfield 1967：120）。 Shoenfield 对 CT2 的看法得到了 Kripke 的赞同。克里普克说，所需要的只是“直接论证”（2013）。此外，Kripke 和其他人（例如 Mendelson 1990）对 CT1 不适合数学处理的公认观点提出了挑战。因此，对CT1的讨论分为两部分：第一部分是通常为CT1提出的证据，假设它是一个无法证明的定义或假设；第二部分是CT1的证据。第二部分是最近尝试用数学论证支持 CT1 的证据。我们可以将第一类证据称为“外部”，第二类证据称为“内部”。接下来的重点是教会在这些发展中的作用。

1.3 CT1的作用

用丘奇的话说，物流系统的决策问题是寻找问题

一个有效的过程，一个决策过程，通过该过程，对于系统的任意wff，可以确定它是否是一个定理（如果是一个定理，则获得它的证明）。 （1956a：273）

丘奇在脚注中指出，从经典的角度来看，附加条件不是必需的，而是朝着直觉主义的“方向”，他将直觉主义描述为“激进的”，但尽管如此，在他的 1956a 的后续部分中，始终包含了附加条件。但这样的决定必须基于有效过程概念的精确对应，例如递归或可定义的过程。如果出现阳性结果，CT2 可以推断存在可计算（有效）程序；如果结果是否定的，则 CT1 允许推断其不存在。这就是 CT 在可计算性理论和逻辑发展中的作用。一个特别有说服力的例子是丘奇对 Entscheidungsproblem（一阶逻辑的决策问题）的否定解，现在称为“丘奇定理”（1936b）。人们认为，至少在原则上，正解将使数学变得完全机械化。原则上每个数学问题都可以通过算法来解决。另一方面，负解的形状是个谜。据报道，冯·诺依曼声称“我们不知道如何证明这一点”（Gandy 1988：62）。丘奇的结果使负解成为可能，并给人们带来了一些希望，即数学问题的解决将继续需要人类的聪明才智。无论如何，诉诸 CT1 有时被视为给出决策问题解决方案的证明的一部分，有时则不然，这取决于所需的形式化程度。例如，证明某些公理理论是不可判定的，就是证明它的定理集不是递归的（或者不是图灵可计算的，等等），而对 CT1 的诉求通常是在严格的数学工作之后出现的。然而，人们并不普遍认为直觉可计算性的精确对应物实际上应该取代它。尽管哥德尔接近这种观点（在图灵可计算性的情况下），但这不是标准观点。其他将直观概念简化为数学术语的做法通常被视为替代方案（参见 Mendelson 1990）；但在丘奇的论文中，这种观点遭到了抵制，否则逻辑学家早就应该停止谈论直观可计算性（有效可计算性）了。

然而，与其他数学一样，可计算性理论的重大发展通常以非正式数学的形式出现。给出了一种非正式的计算方法，很明显它可以被正式的方法取代，尽管这样的演示可能被认为是不必要的或麻烦的。举一个简单的例子：克雷格定理的证明，即任何递归可枚举公式集都是递归公理化的，通常采用非正式论证的形式，即克雷格公理集是可判定的；然后应用 CT1 得出其是递归的结论（参见 Craig 1953）。 Rogers (1967) 给出了许多非形式数学与 CT1 在可计算性理论中的作用的例子。事实上，罗杰斯的经典著作使用了非形式数学以及丘奇的正（非逆）形式的论文来发展整个递归函数论。相比之下，Davis (1958) 给出了完全正式的解释，因此主要以其反证形式使用 CT1，或者等效地，以其正形式但基于还原假设。 CT1 的第三个作用是证明某些基本集合和关系是递归的。例如，标准形式化语言的公式集中的成员资格是直观可计算的。因此，根据 CT1，它一定是递归的，但证明它是递归的证明可能非常复杂（参见 Boolos et al. 2007：Ch. 15）。

1.4 外部证据

CT1 外部证据的经典描述是由 Kleene (1952: 318-323) 提出的。克莱恩将证据分为四个标题：

(一)

启发式证据，

(二)

不同配方的等效性，

(三)

图灵的图灵机概念，以及

(四)

符号逻辑和符号算法。

(A) 的事实是，大族函数已被证明是可定义的，因此是递归的。 (B) 是一个惊人的事实，即可计算性的各种数学上精确的对应物——λ-可定义性、递归性、图灵可计算性以及哥德尔和波斯特时期的其他可计算性——尽管在技术上彼此截然不同——结果却导致了同一类函数。 （并不是每个人都对这种定义的“融合”印象深刻；参见 Kreisel 1987。）至于（C），Kleene 观察到图灵的分析构成了对人类计算机行为给出数学解释的直接尝试，因此不同于其他分析（在递归性和 λ 可定义性方面），后者“以不同的方式出现”。他评论说，图灵将直观可计算性与（图灵）机器的可计算性等同起来，构成了“丘奇论文的独立陈述”。因此，CT1 被称为丘奇-图灵论文。 Church (1937b) 和 Kleene (1952) 也指出 Post (1936) 独立地给出了与图灵非常相似的分析。那么，也许 CT1 应该被正确地称为丘奇图灵后论文。

Kleene 的 (D) 由 Church 之前提到的两个论点组成（1936a：第 7 节）。第一个论点是，通过算法进行计算的概念不会超出递归函数的类别（参见 Shoenfield [1967: 120] 对于相同类型的论点）。第二个涉及递归函数和“符号逻辑”形式系统之间的关系。 Church 认为，在任何这样的定理集可递归枚举的系统中，如果 f 是正整数的一元（“奇数”是 Church 的术语）函数，并且如果

f(m)=n,

对于整数 m 和 n，那么（本质上）(*) 在系统中是可证明的；如果 (*) 为假，则它在系统中不可证明，则 f 是递归的。有关这一有争议论点的更详细讨论，请参阅补充 A.2——之所以有争议，是因为 Church 简单地假设符号逻辑的公理和规则集必须是递归的，而这在一些人看来似乎回避了 CT1 的真实性问题，从而构成了接受 Church 论点的“绊脚石”（Sieg 1997）。

1.5 内部证据

门德尔森对 CT1 不受数学处理的观点提出了质疑，他列举了直观概念实际上被相应的数学精确概念所取代的案例。例如，极限概念是由熟悉的 epsilon-delta 定义给出的，这不仅仅是一个论题。该定义取代了直观概念（Mendelson 1990）。其他人则走得更远，认为可计算性可能被视为一个受公理化处理的原始概念，正如哥德尔曾经建议的那样（根据丘奇给克莱恩的信，1935d [BE：1000]）。西格根据图灵对计算者（“计算机”）的分析提出了公理化。在他的（1936）的第 9 节中，图灵认为（论点 I）图灵机是计算机的一个很好的模型，因此受到某些约束，例如

计算机的行为完全由观察到的符号和计算机的心态决定；

任何时候观察到的符号数量都是有限的；

任何时候只涉及有限数量的心理状态（Gödel [1972]对此条件提出了争议）；和

每个新观察到的符号都在先前符号的有限多个步骤内。

Sieg 以 Gandy 的工作为基础，制定了与这些条件相对应的公理，并声称这些公理化构成了可计算性的公理化（Gandy 1988；Sieg 1997）。

在最近的一篇论文（2013）中，Kripke 认为 CT 可以被视为一阶逻辑完备性定理的“特殊推论”。克里普克的论点让人想起 Kreisel (1987) 早些时候提出的论点，它涉及的不是 CT，而是非正式有效性与形式有效性和可证明性之间的关系。首先考虑 Kreisel 的论点，然后再考虑 Kripke 的论点是有用的（以下一些细节不是 Kreisel 的）：

令 TA、VA 和 DA 分别表示 A 是“仅凭形式”直观有效的非正式论证的一阶翻译，根据一阶逻辑有效性的标准模型理论定义，A 是有效的，并且 A 在一阶形式演绎系统 D 中是可推导的，在通常意义上是健全和完整的。那么非正式地，我们有 DA 意味着 TA。如果一个论证在形式上是可推导的，我们就认为它仅因其形式而有效。至少这是经常教给学生的。而且 TA 也意味着 VA——也教给学生的东西。就完整性而言，VA 意味着 DA。因此，对于一阶逻辑的情况，TA（一个非正式的概念）相当于 DA（一个正式的概念）。 （此外，还可以假设任何直观上有效的论证都可以在一阶语言中形式化，但 Kreisel 并不假设这一点。）

现在，克里普克将他的论点总结如下：

假设一个人有任何有效的论证，其步骤可以用一阶语言来陈述。具有恒等性的一阶逻辑的哥德尔完备性定理的直接结果是，论证的前提可以在任何传统的一阶逻辑形式系统中形式化。假定这种系统的证明关系是递归的（可计算的），那么在计算函数（例如，用算术语言）的特殊情况下，紧接着该函数必须是递归的（图灵可计算的）。 （2013：81）

克里普克假设“希尔伯特论文”：

即任何数学论证的步骤都可以用基于一阶逻辑（具有恒等式）的语言给出