邱奇-图灵论题 Church-Turing Thesis (B. Jack Copeland)

首次发表于 1997 年 1 月 8 日;实质性修订于 2023 年 12 月 18 日

邱奇-图灵论题(或图灵-邱奇论题)是可计算性理论中的一个基本主张。它在 1930 年代中期由邱奇和图灵独立提出。这个论题有各种等价的表述。一个常见的表述是,每个有效计算都可以由图灵机(即图灵的抽象计算机,在其通用形式中包含了存储程序全功能数字计算机的基本逻辑原则)来执行。对邱奇-图灵论题的现代重新构想将其转化,将其扩展到基础物理学、复杂性理论、奇特算法和认知科学。然而,重要的是要意识到,现今被称为邱奇-图灵论题的一些论题充其量只是邱奇和图灵提出的论题的_非常_遥远的亲戚。

翻译说明:在本条目中,除非另有说明,德语原著作的翻译由杰克·科普兰、托比亚斯·米尔兹和乔瓦尼·索马鲁加完成,法语原著作的翻译由科普兰和索马鲁加完成。


1. 1936 年的邱奇-图灵论题及其背景

邱奇-图灵论题关注的是在逻辑、数学和计算机科学中使用的“有效”、“系统化”或“机械化”方法的概念。“有效”及其同义词“系统化”和“机械化”是这些学科中的专业术语:它们并不承载日常含义。一个用于实现某种期望结果的方法或程序 M 被称为“有效”(或“系统化”或“机械化”),只有当:

  1. M 以有限数量的确切指令来规定(每条指令都用有限数量的符号表示);

  2. M 将在有限步骤内,如果没有错误地执行,产生期望的结果;

  3. M 可以(在实践或原则上)由人类在没有任何机械帮助的情况下完成,除了纸和铅笔;

  4. M 不要求执行该方法的人类具有洞察力、直觉或创造力。

一个著名的有效方法的例子是对重言式进行真值表测试。原则上,一个机械式工作的人可以成功地将这个测试应用于命题演算的任何公式——只要有足够的时间、毅力、纸张和铅笔(尽管在实践中,对于包含多个命题变量的任何公式,这个测试是行不通的)。

1.1 术语说明

那些声称存在一种有效方法来实现某种结果的说法通常是通过说存在一种获取某种数学_函数_的值的有效方法来表达的。

例如,对于确定命题演算的任何给定公式是否是重言式的有效方法(如真值表方法),用函数术语表达为说存在一种有效方法来获得函数值,称之为 T,其定义域是命题演算的公式集合,对于任何给定公式 x,记作 T(x),根据 x 是否是重言式,其取值为 1 或 0。

1.2 使得有效方法的非正式概念精确化

有效方法或程序的概念是一个非正式的概念,试图表征有效性的尝试,如上所述,缺乏严谨性,因为该方法必须不要求洞察力、直觉或创造力这一关键要求未被详细阐明。

阿兰·图灵在他 1936 年的著名论文中的一个成就是提出了一个形式上确切的谓词,可以用来取代非正式的谓词“可以通过有效方法完成”(邱奇 1936)。阿隆佐·邱奇也独立进行了类似的工作(邱奇 1936a)。

邱奇-图灵论题 提出的替代谓词在表面上彼此非常不同。然而,这些谓词结果被证明是_等价_的,即每个谓词都选择相同的一组数学函数(称之为 S)。邱奇-图灵论题是这样一种断言,即这个集合 S 包含_每一个_函数,其值可以通过满足上述有效性条件的方法或程序获得。

由于还可以证明,在 S 中除了那些值可以通过满足上述有效性条件的方法获得的函数之外,没有其他函数,邱奇-图灵论题允许用形式化主张“存在一种获取函数 f 的值的有效方法”来替换非正式主张“存在一种获取函数 f 的值的有效方法”,或者用与此等价的任何其他形式化主张。

当邱奇-图灵论题用图灵提出的替换概念表达时,适当地将该论题称为“图灵的论题”;当用邱奇提出的一种或另一种形式替换来表达时,则称为“邱奇的论题”。

邱奇提出的正式概念是_图灵机可计算性_。他主张——邱奇-图灵论题——每当存在一种获取数学函数值的有效方法时,该函数就可以被图灵机计算。

逆否命题——相当于上述提到的主张,即在 S 中除了那些值可以通过有效方法获得的函数之外,没有其他函数——很容易被证实,因为图灵机程序本身就是有效方法的规范。人类可以在不运用任何洞察力、直觉或创造力的情况下,按照程序中的指令进行操作并执行所需的操作。

如果邱奇-图灵论题是正确的,那么关于有效方法和程序的存在与不存在的讨论可以在整个数学、逻辑和计算机科学中被关于图灵机程序的存在或不存在的讨论所取代。

图灵在许多地方陈述了他的论题,严谨程度不同。以下表述是其中最易理解的之一:

邱奇-图灵论题

L.C.M.s [logical computing machines: 图灵对图灵机的表达] 可以做任何可以被描述为“经验法则”或“纯粹机械”的事情。 (Turing 1948 [2004: 414])

他补充道:

这已经被逻辑学家们充分确立,他们现在一致认为“通过最小公倍数计算”是这类短语的正确准确表达。(同上。)

1.3 以数字形式阐述的图灵论题的表述

在他 1936 年的论文中,他题为“On Computable Numbers, with an Application to the Entscheidungsproblem”,图灵写道:

尽管本文的主题表面上是可计算数,但定义和研究可计算函数几乎同样容易……我选择了可计算数进行明确处理,因为它涉及的技术最不繁琐。 (1936 [2004: 58])

可计算数是可以逐渐、逐位由图灵机生成的(实)数的十进制表示。例如:

  • 任何十进制表示由有限位数数字组成的数字(例如,109,1.142)

所有有理数,比如三分之一,七分之二等。

  • 一些无理实数,如 π 和 e。

一些实数是_不可计算_的,正如图灵证明的那样。 图灵的证明指出了一些不可计算的实数的具体例子,但从一般的角度来看,很容易理解,一定存在一些实数是任何图灵机无法计算的,因为实数的数量比图灵机程序的数量_多_。 图灵机程序的数量不可能超过自然数的数量,因为程序是可以计数的:第 1 个程序,第 2 个程序,依此类推;但正如康托在 1874 年证明的那样,实数的数量远远超过自然数的数量(康托 1874 年)。

正如邱奇所说,“定义和研究可计算函数几乎同样容易”:在某种意义上,可计算数和可计算函数之间几乎没有什么区别。例如,可计算数.14159…(由 π 中小数点后的数字组成,即 3.14159…)对应于可计算函数:f(1)=1,f(2)=4,f(3)=1,f(4)=5,f(5)=9,…。

除了图灵论题的表述,比如上面提到的那种,图灵还用数字的术语阐述了他的论题:

邱奇-图灵论题指的是所有自然被视为可计算的数字。 (Turing 1936 [2004: 58])

这是我的主张,这些操作(一个 L.C.M.的操作)包括在计算一个数字时使用的所有操作。(邱奇 1936 [2004: 60])

在这两种表述中的第一种,图灵陈述说,每一个能够通过有效方法计算的数字(也就是,“所有自然被视为可计算的数字”)都包括在那些其十进制表示可以逐步被某个图灵机写出的数字之中。在第二种表述中,图灵说,图灵机的操作包括所有一个人类数学家在通过有效方法计算数字时需要使用的操作。

1.4 图灵论题中“可计算”和“计算”的含义

图灵引入他的机器是为了提供对某种人类活动的理想化描述,即繁琐的_数字计算_。直到自动计算机的出现,这是商业、政府和研究机构中成千上万人的职业。这些人类机械工作者实际上被称为“计算者”。人类计算者使用有效的方法来执行一些如今由电子计算机完成的工作的方面。邱奇-图灵论题是关于计算_在 1936 年使用的术语中_,即人类计算(要了解更多信息,请参阅 第 7 节)。

例如,当图灵说,L.C.M.的操作包括所有“在计算一个数字时需要的”时,他指的是“在计算一个数字时需要的人类”,因为那时计算就是这样的。同样,“自然被视为可计算的数字”是指那些被视为可以被人类计算机计算的数字,即完全按照有效方法工作的人类。

1.5 邱奇的论题

在邱奇使用“有效可计算”一词来表示存在一种获取函数值的有效方法时,图灵使用“纯粹机械”一词;而在图灵通过对最小公倍数的可计算性进行分析时,邱奇提出了两种替代分析,一种是基于“递归”概念,另一种是基于“λ-可定义”(λ-definability)的概念。他提出我们需

定义对正整数的有效可计算函数的概念,将其与正整数的递归函数(或正整数的 λ 可定义函数)的概念等同起来。 (邱奇 1936a: 356)

邱奇和克利尼提出了 λ 可定义函数的概念,罗瑟也做出了贡献(Church 1932, 1933, 1935c, 1936a; Church & Rosser 1936; Kleene 1934, 1935a,b, 1936a,b; Kleene & Rosser 1935; Rosser 1935a,b)。如果函数的值可以通过一定的重复替换过程获得,则称该函数为 λ 可定义函数。递归函数的概念随着时间的推移逐渐形成,其中涉及格拉斯曼、皮尔斯、戴德金德、皮亚诺、斯科勒姆、希尔伯特,以及他的“助手”阿克曼和伯奈斯,苏丹、彼得(原名波利策)、埃尔布兰德、克利尼,以及尤其是哥德尔(Gödel 1931, 1934)。λ 可定义函数(正整数)的类和递归函数(正整数)的类是相同的;这是由邱奇和克利尼证明的(Church 1936a; Kleene 1936a,b)。

当图灵得知邱奇在 1936 年提出将有效性与 λ-可定义性等同起来的建议时(在准备自己的论文发表时),他迅速确立了 λ-可定义性的概念和他的可计算性概念是等价的(通过证明“所有…λ-可定义序列…都是可计算的”及其逆否命题;图灵 1936 年[2004: 88ff])。因此,在邱奇的建议中,“正整数的 λ-可定义函数”(同样也是“正整数的递归函数”)这些词可以被“图灵机可计算的正整数函数”替换。图灵证明的内容被称为_等价结果_。在 4.1 节 中进一步讨论了等价结果。

后来提到了邱奇将有效可计算性与递归性和 λ-可定义性等同起来作为一个“工作假设”,他对邱奇将这一假设伪装成_定义_进行了恰当的批评

[T]o mask this identification under a definition … blinds us to the need of its continual verification. (Post 1936: 105) [T]o mask this identification under a definition … blinds us to the need of its continual verification. (Post 1936: 105)

这, 那么, 就是邱奇提出的“工作假设”

邱奇-图灵论题

一个正整数函数只有在 λ 可定义(或等效地,递归)时才能有效计算。

逆向蕴涵,即正整数的每个 λ 可定义函数都是有效可计算的,通常被称为_邱奇论题的逆命题_,尽管邱奇本人并未做出这样的区分(在他的“定义”中将这两个命题捆绑在一起)。

如果将注意力集中在正整数函数上,邱奇-图灵论题和图灵论题在_外延_上是等价的。“外延等价”意味着这两个命题涉及同一类函数:鉴于邱奇、克林和图灵之前提到的结果,λ-可定义函数(正整数)的类与递归函数(正整数)的类以及可计算函数(正整数)的类是相同的。请注意,虽然从这个意义上说这两个命题是等价的,但它们仍然具有不同的_含义_,因此是两个_不同_的命题。两者之间的一个重要区别是图灵的命题涉及_计算机_,而邱奇的则不涉及。

关于“邱奇-图灵论题”和“图灵论题”这两个术语的起源,克里恩似乎是第一个在这方面使用“论题”一词的人:1952 年,他引入了“邱奇论题”这个名称,用于表明每个可有效计算的函数(自然数上)都是递归的(Kleene 1952: 300, 301, 317)。术语“邱奇-图灵论题”似乎也是由克里恩首创的,带有对他的导师邱奇的偏袒之意:

因此,邱奇和图灵的论题是等价的。我们通常会将它们称为_邱奇论题_,或者在涉及“图灵机”之一的版本时称为_邱奇-图灵论题_。(Kleene 1967: 232)

一些人更喜欢使用名称 邱奇-图灵论题

1.6 比较邱奇和图灵方法

图灵和邱奇方法的一个不同之处在于,邱奇的关注范围比邱奇更广泛,因为(正如刚才提到的),邱奇只考虑正整数的函数,而图灵则将他的工作描述为“整数变量或实数或可计算变量的可计算函数,可计算谓词等等”(1936 [2004: 58])。图灵原打算在随后的一篇论文中探讨实变量的可计算函数理论,但实际上并未这样做。

一个更大的区别在于图灵的方法对于新兴的自动计算科学的深远意义。邱奇的方法没有提到计算机器,而图灵引入了“图灵机”(正如邱奇在他 1937 年评论图灵 1936 年论文时所称)。图灵的论文还介绍了他所称的“通用计算机”。现在被称为通用图灵机,这是图灵的通用计算机。通用机器能够模拟任何单用途图灵机的行为,即为解决一个特定问题而设置的任何图灵机。通用机器通过在其磁带上存储另一台机器的描述来实现这一点,这些描述以一系列指令的有限列表的形式呈现(用现代术语来说,就是计算机程序)。通过遵循适当的指令,通用机器可以执行任何有效的程序,假设邱奇-图灵论题成立。抽象通用机器的功能部分是:

  1. 存储指令和数据的内存,和

  2. 阅读并遵守指令的控制机制。

在那方面,通用图灵机是几乎每台现代电子数字计算机的基本逻辑模型。

在他对图灵的工作进行评论时,邱奇指出了图灵对有效性分析的优势,超过了他自己的优势

可由图灵机计算...的优点在于立即使得与普通(未明确定义)意义上的有效性的识别变得明显。(邱奇 1937a: 43)

他还说,图灵的分析比他自己的(邱奇 1941: 41)“更具直观吸引力”。

哥德尔发现图灵的分析优于邱奇的。 Kleene 提到,直到他看到图灵的阐述,哥德尔才被邱奇的论题说服。

根据 1935 年 11 月 29 日我收到的邱奇写给我的信中,哥德尔认为邱奇提出使用 λ-可定义性作为有效可计算性定义是“完全不令人满意”的。...似乎只有在图灵的阐述出现后,哥德尔才接受了邱奇的论题。(Kleene 1981: 59, 61)

哥德尔描述了图灵对可计算性的分析为“最令人满意”和“正确...毫无疑问”(哥德尔 1951: 304 和 193?: 168)。他评论道:

我们在邱奇之前并没有清晰地理解机械程序的概念,他带领我们走向了正确的视角。(引自王 1974: 85)

哥德尔也说道:

由邱奇-图灵机可执行的概念的明确概念的定义是正确且独特的。(摘自王 1996: 203)

而:

此外,任何理解问题并了解图灵定义的人都绝对不可能为不同的概念做出决定。 (邱奇-图灵论题)

即使是谦逊的年轻图灵也同意他的分析“可能更具说服力” (邱奇-图灵论题 1937: 153)。

1.7 决策问题

邱奇-图灵论题 邱奇和图灵在攻击所谓的_Entscheidungsproblem_时分别提出了各自版本的邱奇-图灵论题。正如前面提到的,图灵 1936 年的论文标题中包含“with an Application to the Entscheidungsproblem”,而邱奇在 1936 年的论文标题中只写了“A Note on the Entscheidungsproblem”。那么,_Entscheidungsproblem_是什么?

德语单词“Entscheidungsproblem”意为_decision problem_。逻辑演算的_Entscheidungsproblem_是设计一种有效方法来决定一个给定公式——任何公式——是否可在该演算中被证明的问题。(这里的“可证明”意味着该公式可以通过演算的公理和定义,仅使用演算的规则,逐步推导出来。)例如,如果用于经典命题演算的这种方法来测试公式 A→A(A 蕴含 A),输出将是“是,可证明”,如果测试矛盾 A&¬A,输出将是“不可证明”。这样的方法被称为_decision method_或_decision procedure_。

邱奇和图灵针对一个名为(一阶)函数演算_的基本重要逻辑系统提出了_Entscheidungsproblem。函数演算包括标准命题逻辑和标准量词逻辑。函数演算也被称为_古典谓词演算_和_量化理论_(有时邱奇使用德语术语_engere Funktionenkalkül_)。他们都得出了相同的否定结果,根据邱奇-图灵论题的论据,即在函数演算的情况下,_Entscheidungsproblem_是_无法解决_的——对于演算来说,没有决策方法。两人独立发现了这一结果,分别在 1936 年发表(邱奇比图灵早几个月)。由于邱奇的证明没有涉及计算机,因此有时被认为比图灵的证明更不那么有趣。

Entscheidungsproblem 吸引了二十世纪初期数理逻辑领域一些最杰出的思想家,包括 Gödel、Herbrand、Post、Ramsey 以及希尔伯特和他的助手 Ackermann、Behmann、Bernays 和 Schönfinkel。Herbrand 将_Entscheidungsproblem_描述为“数学中最一般的问题”(Herbrand 1931b: 187)。但正是希尔伯特将函数演算中的_Entscheidungsproblem_推上了舞台。1928 年,他和 Ackermann 将其称为“数理逻辑的主要问题”(Hilbert & Ackermann 1928: 77)。

希尔伯特知道命题演算(这是函数演算的一个片段)是可决定的,他与伯奈斯找到了一个基于所谓“正规形式”的决策过程(Bernays 1918;Behmann 1922;希尔伯特和阿克曼 1928:9-12;扎赫 1999),他也从勒文海姆的工作中知道单调函数演算是可决定的(Löwenheim 1915)。 (单调函数演算是涉及仅一位谓词的片段,即没有关系,如“=”和“<”,也没有更高位的谓词,如“-在-和-之间-”。)他认为整个函数演算必须有一个决策过程。数理逻辑的挑战,主要问题是找到它。正如他和阿克曼在 1928 年所写的那样,在他们著名的书《理论逻辑基础》(数理逻辑原理)中:

[我]可以预料到,对逻辑公式进行系统的、可以说是计算的处理是可能的.... (Hilbert & Ackermann 1928: 72)

然而,他们的期望在 1936 年的邱奇-图灵论题中受挫。希尔伯特和阿克曼从他们书的修订版中删除了引述的声明。这本 1938 年出版的新版本在很大程度上被淡化,以考虑图灵和邱奇的重大成果。

希尔伯特当然知道,一些数学问题是没有解的,例如寻找一个有限的二进制数 n(或者在希尔伯特版本中是一进制数)使得 n2=2 的问题(希尔伯特 1926 年:179)。他仍然非常喜欢说每个数学问题都可以解决,他的意思是邱奇-图灵论题

每个明确的数学问题必须能够得到确切的解决,要么以对所提出问题的实际回答的形式,要么通过证明其解决的不可能性以及所有尝试的必然失败。 (Hilbert 1900: 261 [trans. 1902: 444])

这似乎从未在他的脑海中闪过,即他的“Hauptproblem der mathematischen Logik”属于这两类中的第二类,直到邱奇和图灵意外地证明了“其解决的不可能性”。

有关 Entscheidungsproblem 的更多细节,以及邱奇和图灵在 1936 年独立建立的惊人结果概述,请参阅 《 Entscheidungsproblem 的兴起与衰落》

2. 背景:_有效方法_和_决策方法_概念的出现

有效方法是邱奇-图灵论题的主题。在邱奇和图灵之前,这个主题是如何演变和详细阐述的?本节回顾了一个早期时代,之后 第 3 节 转向现代发展。

2.1 从简单的经验法则到 Siri 及更高级的应用邱奇-图灵论题

有效的方法在执行许多实际任务时非常有帮助,它们的使用可以追溯到古代的迷雾中,尽管直到二十世纪才开始对它们的本质进行分析。也许最早被利用的有效方法是各种算术计算的经验法则(正如图灵所称),但无论它们起源多么卑微,有效方法的范围在几个世纪内得到了显著扩大。在中世纪,加泰罗尼亚哲学家 Llull 设想了一种有效的方法,用于提出和回答关于上帝属性、灵魂本质、善的本质以及其他基本问题的问题。三百年后,在十七世纪,霍布斯断言人类的推理过程仅仅相当于(基本上是算术的)有效程序:

通过推理,我理解计算。(Hobbes 1655 [1839]: ch. 1 sect. 2)

如今,有效的方法——算法——是电子计算机进行的每项工作的基础。根据一些计算机科学家的说法,有效方法设计的进步将很快引入人类水平的人工智能,随后是超人类智能。已经有虚拟助手如 Siri、Cortana 和 ChatGPT 实施有效方法,为各种问题提供有用答案。

在其最崇高的一般形式中,Entscheidungsproblem_是设计一种有效的通用问答者的问题,一种能够对_任何_有意义的科学问题,甚至是伦理和形而上问题给出正确答案的有效方法。这样一种方法的概念几乎令人瞠目结舌。卢尔(Llull)似乎已经瞥见了一种通用问答方法的概念,在大约 1300 年写道一个通用艺术( ars )或技术,“通过这种方法,人们可以了解所有自然事物”( Lo Desconhort ,第 8 行,见卢尔 1986 年:99)。他梦想着一种_ars generalis(通用技术),可以使“一个通用科学机械化,其具有自己的一般原则,其他科学的原则将被包含其中”(《通用最终艺术》前言,见卢尔 1645 年[1970:1])。卢尔用有限的知识领域来阐明他关于机械问答者的想法,设计了由叠加的圆盘组成的小领域特定机器;他的机器可能采用了羊皮_volvelle_的形式,这是金属星盘的近亲。

在早期现代时代,Llull 的_ars generalis_的想法在莱布尼茨的著作中得到了同情的讨论。

2.2 莱布尼茨

莱布尼茨设计了一台计算机,据说可以进行加法、减法、乘法和除法,并且在 1673 年在伦敦和巴黎展示了他的机器的一个版本(Leibniz 1710)。他对机械方法的兴趣使他产生了更宏大的构想,部分灵感来自吕尔关于通用问答机制的模糊但引人深思的推测。莱布尼茨说吕尔“只是揭示了这个想法的表面,但没有看到它的内在部分”(Leibniz 1671 [1926: 160])。莱布尼茨设想了一种方法,就像乘法或除法一样机械化,可以实现 #邱奇-图灵论题#

当人们之间发生争执时,我们可以简单地说:让我们计算一下,毋需多言,以查明谁是正确的。(Leibniz 1685 [1951: 51])

这种方法的基础,莱布尼茨解释道,“我们可以用数字来表示各种真理和结果”,“然后所有推理的结果都可以用数字方式确定”(Leibniz 1685 [1951: 50–51])。他希望这种方法能够像对数学一样适用于“形而上学、物理学和伦理学”(1685 [1951: 50])。他推测这种方法可以通过他所称的_machina combinatoria_,即组合机(Leibniz n.d. 1;Leibniz 1666)来实现。然而,对于他梦寐以求的方法几乎没有取得什么进展,在他去世前两年的一封信中,他写道:

如果我年轻一些或者有才华横溢的年轻人来帮助我,我仍然希望能够创造一种普遍的符号体系,在这种体系中,所有理性的真理都能被归纳为一种演算。(Leibniz 1714 [1969: 654])

在他的理论中,莱布尼茨描述了他所称之为_ars inveniendi_的发现或设计方法。ars inveniendi_的功能是产生科学上迄今未知的真理(Leibniz 1679 [1903: 37]; Leibniz * n.d. 2 [1890: 180]; Hermes 1969)。一个机械的_ars inveniendi_将产生真实的陈述,随着时间的推移,对科学问题的期待答案将会到来(Leibniz 1671 [1926: 160])。拥有普遍的(即完整和一致的)* ars inveniendi ,用户可以输入_任何_有意义且明确的(科学或数学的)陈述 S,机器最终会(正确地)回答“S 为真”或“S 为假”。正如邱奇和图灵在 1936 年的开创性发展所明确的那样,如果_ars inveniendi_被认为是通过一种有效的方法工作,那么就不可能有普遍的_ars inveniendi —— 甚至没有一个仅限于所有数学陈述的_ars inveniendi_,因为这些包括“p 可证明”形式的陈述,甚至是所有纯逻辑陈述。

2.3 逻辑机器

直到二十世纪,逻辑演算的决策方法的现代概念才得以发展。但早期的逻辑学家,包括莱布尼兹,在字面上确实有一种方法的概念,即可以由他们熟悉的机械部件构造的机器执行——如圆盘、销子、杆、弹簧、杠杆、滑轮、旋转轴、齿轮、配重、刻度盘、机械开关、槽板等。

1869 年,杰文斯设计了一台开创性的机器,被称为“逻辑钢琴”(Jevons 1870; Barrett & Connell 2005)。这个名字是因为这台机器有类似钢琴的键盘用于输入逻辑公式。这些公式来自一个涉及四个正项的三段论演算,比如“铁”和“金属”(Jevons 1870)。图灵的同事梅斯设计了一台有影响力的电子逻辑机(Mays & Prinz 1950),他将逻辑钢琴描述为“第一台能够在没有人类干预的情况下执行逻辑推理的工作机器”(Mays & Henry 1951: 4)。

逻辑钢琴实施了一种方法,用于确定从八个术语中抽取的组合中哪些与输入的公式一致,哪些不一致(尽管实际上并非所有一致的组合都被考虑在内)。该机器通过带有字母的木条显示一致的公式,其中大写字母代表正项,小写字母代表负项。杰文斯在曼彻斯特的欧文斯学院展示了逻辑钢琴,该学院现在是曼彻斯特大学,他在那里担任逻辑学教授(Mays&Henry 1953:503)。杰文斯夸大地声称,他的钢琴“明显地表明,机械能够在很大程度上取代逻辑推理所需的思维活动”(杰文斯 1870:517)。

十年后,Venn 发表了我们现在称之为_Venn 图_(Venn 1880)的技术。这种技术满足了在 Section 1 中为有效方法设定的四个标准。用户首先绘制一个三段论的前提,然后,正如 Quine 所说,“我们检查图表,看看结论的内容是否自动出现在图表中”(Quine 1950: 74)。并非所有的函数演算公式都可以用 Venn 图表示,Venn 的原始方法仅限于测试三段论。在二十世纪,Massey 表明 Venn 的方法可以扩展到为单子函数演算提供决策过程(Massey 1966)。

Venn, like Jevons, was well aware of the concept of a literally mechanical method. He pointed out that diagrammatic methods such as his “readily lend themselves to mechanical performance” (Venn 1880: 15). Venn went on to describe what he called a “logical-diagram machine”. This simple machine displayed wooden segments corresponding to the component areas of a Venn diagram; each wooden segment represented one of four terms. A finger-operated release mechanism allowed any segment selected by the user to drop downwards. This represented “the destruction of any class” (1880: 18). Venn reported that he constructed this machine, which measured “between five and six inches square and three inches deep” (1880: 17). When Venn published his description of it, Jevons quickly wrote to him saying that the logical-diagram machine “is exceedingly ingenious & seems to represent the relations of four terms very well” (Jevons 1880). Venn himself however was less enthusiastic, saying in his article “I have no high estimate myself of the interest or importance of what are sometimes called logical machines” (1880: 15). Baldwin, commenting on Venn’s machine in 1902, complained that it was “merely a more cumbersome diagram” (1902: 29). This is quite true—it would be at least as easy to draw the Venn diagram on paper as to set it up on the machine. But Venn’s article made it very plain that the logical-diagram machine was intended to be a hilarious send-up of Jevons’ complicated logic piano.

在大约同一时间,马昆(皮尔斯的学生)设计了一台逻辑机器,然后普林斯顿的一位同事用从“普林斯顿最古老的住宅”中拆下的木头建造了它(马昆在他的 1885 年的著作中提到)。马昆知道杰文斯和文恩的设计,并表示在某些方面他“追随了杰文斯”,他自己的机器“与杰文斯的有些相似”(马昆 1881 年,1883 年:16,1885 年:303)。皮尔斯以他惯有的直率称马昆的机器为“比杰文斯的机器聪明得多的设计”(皮尔斯 1887 年:166)。马昆的设备也仅限于涉及四个肯定术语的三段论演算,与杰文斯的设备一样,显示出与输入公式一致的术语组合。一个带有十六个机械拨轮的字母板用于显示这些组合。

2.4 皮尔斯

1886 年,皮尔斯在写给马昆德的一封信中著名地建议马昆德考虑他的机器的电气版本,并勾画了实现(我们现在称之为)与门和或门的简单开关电路 - 这可能是电气计算的最早提议(皮尔斯 1886 年)。皮尔斯在信中有远见地写道,利用电力,“绝不是没有希望地期望制造一台用于解决非常困难数学问题的机器”。很久以后,邱奇在普林斯顿大学的马昆德文件中发现了一个详细的基于电子继电器的马昆德机器形式的图表(见 Ketner&Stewart 1984:200)。在这个图表中设计的是马昆德、皮尔斯还是一个未知的第三人,都有资格成为重要的早期电机计算的先驱。

皮尔斯对逻辑机器的兴趣似乎是第一个考虑决策问题的人,大致上是图灵和邱奇所解决的形式。从大约 1896 年开始,他发展了他称之为“存在图”的图解证明程序。这些比维恩的图表先进得多。皮尔斯的_阿尔法图_系统是命题演算的图解公式,他的_贝塔图_系统是一阶函数演算的一个版本(皮尔斯 1903a; 罗伯茨 1973)。罗伯茨(1973)证明了贝塔图系统包含奎因 1951 年对一阶函数演算的公理和规则,其中只断言了封闭的公式(奎因 1951: 88)。

皮尔斯在他于 1903 年在波士顿发表的一系列讲座的广泛笔记中预见了决策方法的概念。在那里,他发展了一种方法(皮尔斯 1903b,c),如果应用于命题演算的任何给定公式,他说,“确定”(或“积极确定”)阿尔法图系统是否证明该公式是可满足的(用皮尔斯的术语来说是“阿尔法可能的”),或者,另一方面,系统是否证明它是不可满足的(“阿尔法不可能的”)。 (有关“可满足性”的解释,请参阅 ​*Entschedungsproblem*​的兴起与衰落》 的补充说明。)皮尔斯说他的方法“是如此全面的常规,以至于很容易定义一个可以执行它的机器”——尽管他继续说,“案例的复杂性使得任何这样的程序都相当不切实际”(皮尔斯 1903c)。也许他会对在五六十年内,并且借助电力,变得远非不切实际地在机器上运行命题演算的决策方法并不感到完全惊讶。

皮尔斯还寻找过与他的 β-图系统相对应的方法(皮尔斯 1903b,c,d;罗伯茨 1997)。就像他之后的希尔伯特一样,他似乎毫不怀疑全一阶谓词逻辑可以用机器化的方法来处理。

皮尔斯对数学中机器的使用有着超前的想法。在世纪之交左右,他写道:

整个高等算术科学,以其数百个奇妙定理,实际上是从关于数字的六个基本假设中推导出来的。迄今为止构建的逻辑机器无法执行数学推导。然而,有一种现代精确逻辑,虽然仍处于萌芽阶段,但已经发展得足够先进,使得构建一台能够推导出所有已知算术定理并比现在更快推进该科学的机器只是一个费用问题。 (Peirce n.d. ,引自 Stjernfelt 2022)

这里,皮尔斯似乎在断言——非常正确地——可以设计出一台机器来推导出戴德金德(1888 年)算术公理化的所有定理(其中包括六个“主要假设”,形式为四个公理和两个定义)。这个皮尔斯的论述是在图灵将图灵机引入数学之前近四十年提出的,可以说是超前的。

至于是否所有数学推理都可以由机器执行,正如莱布尼茨所认为的那样,皮尔斯持怀疑态度。他提出了这样一个假设,即在未来,数学推理邱奇-图灵论题

可能留给机器处理——某种巴贝奇的分析引擎或某种逻辑机器。(Peirce 1908: 434)

然而,他将这个假设与他认为的其他“逻辑异端”并列,称其为“恶性”(同上)。 图灵随后的结果(图灵 1936 年,1939 年)可能证明了他持怀疑态度的立场,尽管他持怀疑态度的原因可能并非如此。 但在此之前,在哥廷根的希尔伯特及其团队的影响下,数学家中出现了一种完全不同的看法。

2.5 希尔伯特和哥廷根学派

这在很大程度上是希尔伯特首先引起人们对需要对有效决策方法的概念进行精确分析的注意。在 1917 年他在苏黎世向瑞士数学学会发表的一次讲座中,他强调了研究“有限次操作的可决定性”概念的必要性,并准确地指出这将是“一个重要的新研究领域的发展”(希尔伯特 1917: 415)。这次讲座考虑了他所称的“一些具有特定数学特征的最具挑战性的认识论问题”(1917: 412)。其中最重要的是“一个数学问题的可决定性问题”,因为这个问题“深刻地触及了数学思维的本质”(1917: 413)。

希尔伯特及其哥廷根小组将莱布尼茨视为他们对逻辑和数学基础的方法的创始人。小组的杰出成员贝曼说,莱布尼茨预见了现代符号逻辑(Behmann 1921: 4–5)。莱布尼茨假设的“普遍特征”或通用符号主义是一种通用的符号语言,在概念上类似于今天数学逻辑和计算机科学中使用的语言。希尔伯特和阿克曼在他们的《理论逻辑基础》的第一页上承认了莱布尼茨对他们的影响,称“数学逻辑的概念最初是由莱布尼茨清晰地表达的”(Hilbert & Ackermann 1928: 1)。卡西勒说,在希尔伯特的工作中,“莱布尼茨‘普遍特征’的基本思想被重新提出,并得到了简明而准确的表达”(Cassirer 1929: 440)。正是在哥廷根小组的著作中,莱布尼茨关于回答任何指定数学或科学问题的有效方法的想法得到了最充分的发展(详见有关《决策问题的兴起与衰落》的补充)。

希尔伯特最早提到我们现在称之为决策问题的出版物是他 1899 年的书《几何基础》。他说,在研究欧几里得几何学的过程中,他发现

受到“以讨论每个给定问题的原则指导,我们要审查它是否可以或不可以通过使用某些有限资源的规定步骤来回答。”的启发。 (Hilbert 1899: 89)

关于一个具体的例子,他写道:

假设提出了一个可以用圆规完成的几何构造问题;我们将尝试建立一个标准,使我们能够立即从问题及其解决方案的分析性质中确定,是否也可以仅使用尺和线段传递器来完成构造。 (Hilbert 1899: 85–86)

他描述了现在被称为有效方法来确定这一点,他的术语“beurteilen”可以有点时代错误地翻译为“决定”。

希尔伯特在接下来的一年更清晰地表达了决策方法的概念,在他在巴黎举行的著名的世纪之交的演讲中,向国际数学家大会提出了二十三个未解问题,“可以预期从讨论这些问题中推动科学的发展”。他名单上的第十个问题(现在被普遍称为希尔伯特的第十个问题)是:

给定一个具有任意数量未知量和具有有理整数系数的丢番图方程:设计一个过程,根据这个过程可以通过有限次操作确定方程是否可在有理整数中求解。 (Hilbert 1900: 276 [trans. 1902: 458])

Entscheidungsproblem_在希尔伯特的学生贝曼于 1922 年发表了一篇具有里程碑意义的文章之后变得更加清晰。这篇文章名为《逻辑代数的贡献,特别是_Entscheidungsproblem》。很可能是贝曼创造了“Entscheidungsproblem”这个术语。在 1921 年向哥廷根小组的演讲中,贝曼说道:

如果给出一个逻辑或数学命题,所需的程序应该提供完整的指令,通过有限步骤后的确定性计算来判断该命题是正确还是错误。因此,我想称之为_allgemeine Entscheidungsproblem_ [一般决策问题]。(Behmann 1921: 6 [trans. 2015: 176])

皮尔斯提到了一个程序形成“如此全面的例行程序,以至于很容易定义一台执行它的机器”。他的工作在哥廷根很有名:希尔伯特和阿克曼说皮尔斯“特别”,还有杰文斯,“丰富了数理逻辑这门年轻科学”(1928 年:1)。像皮尔斯一样,贝曼利用机器的概念来阐明_Entscheidungsproblem_的性质。“问题的特性是至关重要的”,贝曼说,“只涉及根据给定指令进行完全机械化的计算”。判断陈述是真还是假变成了“纯粹的计算练习”;“思考被机械计算所取代”。贝曼继续说道:

一个人可能会,如果他愿意的话,谈论机械或类似机器的思维。(也许有一天甚至可以让机器来执行它。)(Behmann 1921: 6–7 [trans. 2015: 176])

莱布尼茨的吕利观念,即一台能够计算真理的机器,突然成为二十世纪早期数学的前沿。

2.6 纽曼和剑桥数学家

Behmann 强调的决策问题与执行“计算练习”的机器之间的联系很快在图灵手中变得至关重要。图灵似乎首次与_Entscheidungsproblem_接触是在 1935 年,当时他在剑桥听了纽曼的一堂讲座。纽曼是一位数理逻辑学家和拓扑学家,对源自哥廷根的思想非常熟悉。早在 1923 年,他就对希尔伯特的一些想法进行了非常独特的讨论,提出了自己对数学基础的一种方法,虽然激进而新颖,但仍然带有强烈的希尔伯特风格(Newman 1923)。1928 年,纽曼参加了在意大利博洛尼亚举行的国际数学家大会,希尔伯特在那里讲解了_Entscheidungsproblem_,同时讲解了他的证明理论(Hilbert 1930a;Zanichelli 1929)。希尔伯特在数理逻辑方面的重要作品——Hilbert and Ackermann(1928)和 Hilbert and Bernays(1934)——都被推荐为纽曼自己关于数学基础的讲座的阅读材料(Smithies 1934;Copeland and Fan 2022)。

在一次录音采访中,纽曼谈到了图灵与邱奇-图灵论题的关系,他说:“我相信一切都始于他参加了我关于数学和逻辑基础的讲座”

我想我在这次讲座中说过,所谓一个过程是建设性的意思是它是一个纯粹的机械装置——我甚至可能已经说过,一台机器可以做到这一点。

I'm sorry, but it seems like your input is empty. Could you please provide the text you'd like me to translate into Simplified Chinese?

而这当然引导[图灵]迎接下一个挑战,什么样的机器,这启发他尝试阐明什么是完全通用的计算机。(Newman _c_1977)

遗憾的是,在他的讲座中那个关键时刻,没有记录纽曼说了什么。然而,他 1923 年的论文《从物理学角度看数学的基础》记录了他的一些相关思想(Copeland & Fan 2023)。在那里,他引入了术语“过程”(他在上面的引文中也使用了),说“所有逻辑和数学都由某些_过程_组成”(1923: 12)。他强调了过程应该以所需的结果(如定理或数字)_终止_的要求;他对过程进行了正式处理:

进程的属性是从一组公理中正式发展出来的,并达到了一种攻击特定进程是否终止的问题的一般方法。 (Newman 1923: 12)

Newman 在他 1923 年的论文中没有提到_Entscheidungsproblem_,更不用说提出它的不可解性(没有证据表明,在图灵之前,他认为这个问题是不可解的)—然而,事后看来,他确实为解决这个问题奠定了一些暗示性的基础。他写道:

关于一个过程或过程部分的首要信息是是否 可能 执行它。[过程] Φ||αρ 的陈述是可能的意味着这个过程_终止_:停止下来…(Newman 1923: 39)

纽曼甚至提出了一种“装置”,一种“符号机器”,通过执行他分析的那种过程来生成数字,并从这一提议的角度深入讨论了实数(1923 年:130 页及以下)。

Newman 并不是剑桥唯一对邱奇-图灵论题感兴趣的人。在图灵着手研究这个问题的前十年,邱奇-图灵论题在剑桥大学备受关注。剑桥大学的数学 Sadleirian 教授 Hardy 对这个问题很感兴趣,受到冯·诺伊曼对希尔伯特思想的权威阐述和批判的启发(冯·诺伊曼 1927 年)。Ackermann 本人于 1925 年上半年从哥廷根访问剑桥大学(Zach 2003: 226)。另一位访问者 Langford 曾在剑桥大学从哈佛大学获得的奖学金支持下工作,于 1924 年至 1925 年学术年度后不久回到哈佛大学,实际上解决了邱奇-图灵论题的一些特殊情况(Langford 1926a, 1927)。

剑桥逻辑学家 Ramsey,像图灵一样是国王学院的研究员,在 20 世纪 20 年代后期也致力于* Entscheidungsproblem 。他于 1930 年去世(就在图灵作为本科生抵达剑桥的前一年),但在去世前完成了一篇解决 Entscheidungsproblem 特殊情况的关键论文(Ramsey 1930)。他的工作也是纽曼讲座课程推荐阅读中的重要内容。Braithwaite,国王学院的另一位研究员(曾在 1935 年帮助图灵当选国王学院的初级研究员),对 Ramsey 在 Entscheidungsproblem 上的工作非常感兴趣(Copeland&Fan 2022)。同样在 1935 年,冯·诺伊曼从普林斯顿访问剑桥,参加纽曼讲座课程的下一个学期(Copeland&Fan 2023)。冯·诺伊曼是 20 世纪 20 年代中期哥廷根学派的成员,曾称 Entscheidungsproblem *为“深奥而复杂”,并表示怀疑其是否可解决(冯·诺伊曼 1927 年:11;1931 年:120)。

他并不孤单。哈代在讨论希尔伯特的观点时提出了这个_Entscheidungsproblem_(决策问题)的论述。

假设,例如,我们能够找到一套有限的规则系统,使我们能够判断任何给定的公式是否可证明。 (Hardy 1929: 16)

Hardy 预见到了邱奇-图灵论题,告诉他的听众,这样一套规则“是不可预期的”。

图灵所展示的是,永远不会有,也永远不可能有,一台符合以下规范的计算机:当用户输入一个公式——任何公式——功能演算中,该机器执行有限步骤,然后输出正确答案,即“此公式在功能演算中是可证的”或“此公式在功能演算中是不可证的”,具体情况而定。因此,鉴于邱奇的论题_如果存在有效方法,则可以由他的机器之一执行_,由此可见,没有有效方法可以决定完整的一阶功能演算。

3. 其他可计算性方法

邱奇和图灵肯定不是唯一一组处理分析有效性概念问题的人。本节概述了二十和二十一世纪提出的其他一些重要建议。

3.1 哥德尔

哥德尔被引导到分析有效性的问题,是因为他在寻找一种方法来_概括_他 1931 年的不完备性结果(这些结果最初只适用于怀特海德和罗素在他们的_数学原理_中阐述的形式系统)。1934 年,他考虑了用他的广义递归概念来进行分析——比教堂首次公开宣布他的论点早大约一年,即“正整数的有效可计算函数的概念应该与递归函数的概念等同”(教堂 1935a;哥德尔 1934,注 3;戴维斯 1982)。

但哥德尔表示怀疑:“当时我并不完全相信我的递归概念包括所有可能的递归”(哥德尔 1965b)。哥德尔强调,正是图灵的分析最终使他能够推广他的不完备定理:

由于邱奇的工作,现在可以给出对形式系统一般概念的精确而无疑地充分定义。(哥德尔 1965a:71)

他解释道:

图灵的工作对“机械过程”(又称“算法”或“计算过程”或“有限组合过程”)的概念进行了分析。这个概念被证明等同于“图灵机”的概念。形式系统可以简单地定义为用于生成公式(称为可证公式)的任何机械过程。 (邱奇 1965a:71-72)

凭借这个定义,哥德尔说,"可以严格证明对于_每个_包含一定量有限数论的一致形式系统来说,不完备性是成立的" (1965a: 71)。

3.2 岗位

到了 1936 年,Post 独立得出了与 Turing 的分析基本相同的有效性分析(Post 1936; Davis & Sieg 2015)。Post 理想化的人类“工作者”——或“问题解决者”——在由“一系列双向无限的空间或盒子”组成的“符号空间”中运作。一个盒子接受

只有两种可能的状态,即为空或未标记,并且在其中有一个标记,比如一个竖直的笔画。 (Post 1936: 103)

问题解决者按照“一组固定不变的指令”进行工作,并且可以执行少量的“原始行为”(Post 1936: 103),即:

确定当前占用的方框是否被标记。

  1. 擦除当前被占用的方框中的任何标记;

  2. 如果未标记,请标记当前被占用的方框。

  3. move to the box to the right of the present position; and -> 4. 移动到当前位置右侧的方框;并

  4. move to the box to the left of the present position. 5. 移动到当前位置左侧的方框。

Post 的论文于 1936 年 10 月提交发表,比图灵晚了大约五个月。这篇论文中没有图灵通用计算机的类似物,也没有预料到邱奇和图灵的结果,即_Entscheidungsproblem_是无法解决的。然而,耐人寻味的是,Post 在 1936 年的论文中所取得的成就远远超出了他的交代。在一篇名为“一次预见的叙述”的文章中(发表于 1965 年,但大约是 1941 年写的),他解释说在 20 世纪 20 年代初期,他设计了一个系统——他称之为“完全正常系统”,因为“在某种程度上,它包含了所有正常系统”,他说,这“对应”于图灵的通用机(Post 1965: 412)。此外,他在同一时期辩称,在他的“正常系统”情况下,决策问题是无法解决的(1965: 405ff)。但似乎他没有将这一论点扩展到预料到邱奇-图灵论题,即谓词演算的决策问题是无法解决的(1965: 407)。

图灵后来慷慨地承认了 Post 在 1936 年发表的论文,将图灵机描述为“由 Post 和作者引入的逻辑计算机”(Turing 1950b: 491)。

3.3 希尔伯特和伯奈斯

1939 年,在他们庞大的著作《数学基础》第二卷中,希尔伯特和伯奈斯提出了基于逻辑的有效性分析。根据这一分析,可有效计算的数值函数是可以以他们所称的“regelrecht”方式进行评估的数值函数(Hilbert&Bernays 1939:392-421)。在这个背景下,德语词“regelrecht”可以翻译为“rule-governed”。希尔伯特和伯奈斯提出了数值函数的_rule-governed evaluation_概念作为“可计算概念的深化”(1939:417)。

基本思想是:以规则为基础的方式评估数值函数(如加法或乘法)是逐步逻辑地计算函数的值,在适当的演绎逻辑系统中。根据这种方法,有效可计算性被分析为_逻辑中的可计算性_。(邱奇和图灵之前曾讨论过这种方法—请参见 第 4.4 节。)

邱奇-图灵论题中使用的逻辑系统是_等式演算_,类似于哥德尔在 1934 年在普林斯顿的讲座中详细介绍的演算(哥德尔 1934)。等式演算的定理(正如其名称所示)是_方程_——例如 23=8 和 x2+1=x(x+1)−(x−1),或者一般地说 f(m)=n。希尔伯特-伯奈斯等式演算不包含逻辑符号(如否定、合取、蕴涵或量词),每个公式只是项之间的一个方程。三种类型的方程被允许作为系统中推导的初始公式(或前提),并且系统需要满足希尔伯特和伯奈斯称之为“递归条件”的三个一般条件。演算的规则涉及方程内的替换,非常简单,允许诸如:

a=b, f(a)⊢f(b) translates to a=b, f(a)⊢f(b)

根据这个微积分(他们称之为 Z0),希尔伯特和伯奈斯建立了一个等价结果:能够进行规则评估的数值函数与(原始的)递归函数相一致(1939 年:403 和 393_n_)。

这也许并不令人意外,作为证明理论创始人的希尔伯特最终选择了将有效可计算性的分析作为_逻辑内的可计算性_,尽管邱奇和图灵分别已经提出了他们关于递归函数和图灵机的分析。希尔伯特和伯奈斯继续运用他们的分析,给出了一个新的证明,证明了_判定问题_的不可解性(希尔伯特和伯奈斯 1939: 416-421)。这一证明悄然标志着对他们来说必定是一次令人不安甚至痛苦的视角转变。在邱奇-图灵结果出现之前,数学的决策程序的概念一直是他们思考的核心,而在 1934 年出版的《Grundlagen》第 1 卷中,他们假定_判定问题_是可以解决的。

3.4 现代公理分析

邱奇报告了他与哥德尔的讨论,当时关于如何形式化有效可计算性的直观概念还没有明确方向(可能是在 1934 年期间)。哥德尔建议说

可能是可能的,在有效可计算性作为一个未定义的概念方面,陈述一组公理,这些公理将体现这个概念的普遍接受的属性,并在此基础上做一些事情。 (邱奇 1935b)

逻辑学家经常通过陈述一组共同体现(比如)普遍量化的普遍接受的特性的公理来分析一个感兴趣的概念,而不是通过用其他概念来定义它。要在效率的情况下采用这种方法,我们会“写下一些关于可计算函数的公理,大多数人都会同意这些公理显然是真实的”(Shoenfield 1993: 26)。Shoenfield 继续说,“可能可以从这些公理中证明出邱奇-图灵论题”,但他补充说:“然而,尽管努力,没有人成功做到这一点”。

继续前进几年,于千禧年之交举行的关于《二十一世纪数理逻辑前景》的会议中,以下问题被列为主要的未解问题:

“通过找到直观明显或至少是清晰可接受的计算属性来“证明”邱奇-图灵论题,这些属性足以保证任何如此计算的函数都是递归的【因此可以被图灵机计算】。”(Buss 等人,2001 年:174-175)

邱奇-图灵论题的公理化方法,如哥德尔所勾勒的,目前已经以多种完全不同的方式发展起来。这些公理化框架在很大程度上有助于消除蒙塔古 60 多年前的抱怨:“教会论题的讨论因缺乏一个可以进行讨论的精确的一般框架而受到影响”(Montague 1960: 432)。公理化方法的一些示例如下(按时间顺序):

  • Gandy(图灵的唯一博士生)指出,图灵对人类计算的分析并不立即适用于与图灵机大不相同的计算机。有关图灵分析的详细信息,请参见下文 第 4.3 节。例如,图灵的分析显然不适用于并行机,与图灵机不同,它们能够同时处理任意数量的符号。Gandy(1980)寻求了一种广义的图灵分析形式,既适用于图灵机又适用于大规模并行机,他提出了规定所谓_离散确定性机械装置_行为的四个公理。(他用继承有限集的术语制定了这些公理。)然后,Gandy 证明了满足这些公理的每个装置都可以被图灵机模拟:离散确定性机械装置,即使是大规模并行装置,在某种意义上也不比图灵机更强大,因为这样的装置能够执行的任何计算也可以被通用图灵机完成。(有关 Gandy 的分析,请参见 第 6.4.2 节。)

Engeler 通过使用_组合子_(Engeler 1983: ch. III)对算法函数的概念进行了公理化。组合子最初是由 Schönfinkel 于 1924 年引入的,在一本关于组合子的最新书中被描述为“首次提出了通用计算的形式化”(Schönfinkel 1924; Wolfram 2021: 214)。Schönfinkel 的组合子得到了 Curry 的广泛发展(Curry 1929, 1930a,b, 1932; Curry & Feys 1958)。组合子的例子包括“置换器”C 和“取消器”K。这些产生以下效果:Cxyz=xzy 和 Kxy=x。

  • 邱奇 formalized 图灵对人类计算的分析,通过四个公理(Sieg 2008)。结果,邱奇说,这是对“‘机械程序’概念”的公理化描述,并且他观察到他的系统“证实了哥德尔的评论”(上文),即应该尝试找到一个包含普遍接受的有效性概念属性的公理集(Sieg 2008: 150)。

  • Dershowitz 和 Gurevich(2008)陈述了三个非常一般的公理,将计算视为离散的、确定性的、顺序演变的状态结构。他们将这些结构称为“状态转移系统”,将这三个公理称为“顺序公设”。他们还使用了第四个公理,规定“初始状态只能使用不可否认的可计算操作”(2008:306)。从他们的四个公理中,他们证明了一个命题,称为邱奇-图灵论题:“由满足顺序公设的状态转移系统计算的每个数值函数,并且初始只提供基本算术,都是部分递归的”(2008:327)。

回到证明邱奇-图灵论题的_核心思想_,重要的是要注意,德肖维茨和古列维奇所称的邱奇论题实际上并非邱奇所陈述的论题,即“仅当递归时,正整数函数才能有效计算”。至关重要的是,他们对邱奇论题的版本甚至没有提及有效计算的关键概念。试图证明邱奇(或图灵)的实际论题的整个项目存在其份量的哲学困难。例如,假设有人提出一些关于有效计算的主张的公理(就像西格所做的那样),并且假设可以从这些公理中证明正整数函数仅当递归时才能有效计算。邱奇论题将会从这些公理中被证明,但这些公理是否构成了对有效计算的令人满意的解释是一个_进一步_的问题。如果不是,那么这种对邱奇论题的“证明”将无法令人信服。也就是说,这种证明只会对那些接受另一个论题的人具有说服力,即这些公理确实是对有效计算的令人满意的解释。这是一个邱奇式的元论题。邱奇论题将会被证明,但只是以提出另一个未经证实的论题为代价,这个论题似乎具有相同性质。

4.3.5 节4.5 节4.6 节 中进一步讨论了与证明邱奇-图灵论题相关的困难。

4. 邱奇-图灵论题的论据

4.1 归纳和等价论证

尽管有时会有人试图质疑邱奇-图灵论题(例如卡尔马尔在 1959 年的尝试;门德尔逊在 1963 年回应),但图灵在 1948 年给出的总结至今仍然成立:“逻辑学家现在一致认为‘可由逻辑计算机解决’是对效率非正式概念的正确准确诠释”。

在 1936 年,邱奇和图灵分别提出了接受各自论题的各种理由。邱奇辩称:

事实是,两种如此广泛不同且(在作者看来)同样自然的有效可计算性定义【即,用 λ-可定义性和递归来定义】竟然被证明是_等价的_,这加强了下文提出的理由的力量,使人相信它们构成了对这一概念的一种一般性描述,这种描述符合通常的直观理解。(邱奇 1936a:346,强调添加)

邱奇的“下文提出的理由”包括两个并非完全令人信服的论点。两者都受到相同的弱点困扰,详见 Section 4.4.4

图灵则为这个论题提出了强有力的论据。与邱奇不同,他为此提供了归纳证据,展示了大类数字“自然被视为可计算”的可计算性(1936: 74–75)。例如,图灵证明了可计算收敛序列的极限是可计算的;所有实代数数都是可计算的;贝塞尔函数的实零点是可计算的;以及(如前所述)π 和 e 是可计算的(1936: 79–83)。但最重要的是,图灵为这个论题提出了深刻的逻辑-哲学论证。他简单地将这些论证称为“I”、“II”和“III”。它们在 Section 4.3Section 4.4 中描述。

到了大约 1950 年,已经积累了大量支持这一论题的证据。对这些证据进行了最全面调查之一可在克里恩 1952 年的第 12 章和第 13 章中找到。除了讨论图灵的第一个论证和以上提到的邱奇的两个论证外,克里恩加强了邱奇刚才引用的_等价论证_,指出“几种其他特征...已经被证明是等价的”(1952: 320)。除了邱奇提到的特征之外,克里恩还包括了图灵机的可计算性,Post 的规范系统和正常系统(Post 1943 年,1946 年),以及哥德尔的可计算性概念(哥德尔 1936 年)。(图灵的学生兼终身朋友罗宾·甘迪形象地称邱奇的等价论证为“汇流论证”[甘迪 1988: 78]。)

在现代,等价论证可以更有力地提出:所有试图对有效可计算函数的直观概念给出精确描述的尝试都被证明是_等价的_,即每个提出的描述都被证明选择了相同的函数类,即那些可以被图灵机计算的函数。等价论证通常被认为是这个论题非常有力的证据,因为涉及到的各种形式化描述的_多样性_。除了在 第 1 节第 3 节 中已经提到的许多不同描述外,还有基于寄存器机的分析(Shepherdson & Sturgis 1963)、马尔可夫算法(Markov 1951)和其他形式化方法。

等价论证可以通过以下方式概括:有效可计算性的概念,或者简单地说可计算性的概念,已经被证明是超越形式主义的,甚至是“无形式主义的”(Kennedy 2013: 362),因为所有这些不同的形式方法都准确地确定了_相同_的函数类。

实际上,在任何给定的形式方法中,甚至没有必要区分不同阶或类型的系统。哥德尔在 1936 年发表的一篇摘要中指出,“可计算”的概念是_绝对_的,即所有可计算函数都可以在同一个系统中指定,无需引入不同阶层系统的层次结构——例如,在塔斯基对“真实”概念的分析中,以及在“可证明”概念的情况下通常如此(哥德尔 1936: 24)。十年后,在评论图灵的工作时,哥德尔强调了“图灵的可计算性”的重要性。

主要是因为这个概念首次成功地给出了一个有趣的认识论概念的绝对定义,即不依赖于所选择的形式主义。在先前处理的所有其他情况中,如可证明性或可定义性,人们只能相对于给定语言来定义它们.... (邱奇-图灵论题 1946: 150)

在他 1952 年的调查中,Kleene 还发展了图灵的归纳论证(1952: 319-320)。要总结:

每个在这方面被研究过的有效可计算函数都被证明可以被图灵机计算。

所有已知的从给定的有效可计算函数获取新的有效可计算函数的方法或操作,都可以通过从给定的图灵机构造新的图灵机的方法来实现。

归纳证据继续积累支持这一论题。例如,Gurevich 指出邱奇-图灵论题

就输入输出关系而言,同步并行算法和交互式顺序算法可以被图灵机模拟。这进一步证实了邱奇-图灵论题。(Gurevich 2012: 33)

4.2 对归纳和等价论证的怀疑

这是归纳论证的一般特征,虽然它们可能提供强有力的证据,但它们仍然不能确定地证实它们的结论。对于邱奇-图灵论题来说,需要一个更有力的论证。甘迪说归纳论证

无法解决哲学(或基础)问题。可能有一天,某位天才建立了一种全新的计算方式。(Gandy 1988: 79)

Dershowitz 和 Gurevich 强调了困难:

历史上充满了延迟发现的例子。 亚里士多德和牛顿力学的持续时间远远超过了自邱奇提出将有效性与递归性等同的七十年,但最终这些物理理论还是被发现有所欠缺。 (Dershowitz & Gurevich 2008: 304)

Dershowitz 和 Gurevich 提出了一个延迟发现的高度相关示例(参考 Barendregt 1997: 187):任何希望有效可计算函数能够与 1923 年引入的_原始_递归函数(Skolem 1923; Péter 1935)等同的希望在几年后消失了,当 Ackermann 描述了一个有效可计算的函数,而这个函数并非原始递归函数(Ackermann 1928)。

等价论证也被认为是不令人满意的。德肖维茨和古列维奇称其为“弱”(2008: 304)。毕竟,一些陈述是等价的这个事实并不能表明这些陈述是真实的,只能表明如果其中一个是真的,那么所有的都是真的——如果其中一个是假的,那么所有的都是假的。克赖塞尔写道:

邱奇-图灵论题的支持...当然并不在于...不同特征的等价性:排除了_系统性_错误的情况?(Kreisel 1965: 144)

Mendelson 更温和地表达了这一观点,称等价论证“并非决定性的”

这是可以想象的,所有等价概念定义了一个与有效可计算性相关但并非完全相同的概念。 (Mendelson 1990: 228)

显然,所需的是从第一原理出发对这个论题进行直接论证。邱奇的论证填补了这一角色。

4.3 图灵的论证 I

邱奇-图灵论题在《可计算数的论题》第 9 节中提出的逻辑-哲学论证是接受这一论题的重要理由之一。

他将论证 I 称为他 1936 年论文开头的评论的“仅仅是一个阐述” - 例如:

我们可以将计算实数的过程中的人与一台只能具有有限数量条件 q1,q2,…,qR 的机器进行比较,这些条件将被称为“m-配置”。(邱奇-图灵论题 1936 [2004: 59, 75])

他还将论证 I 描述为“对直觉的直接呼吁”(邱奇 1936 [2004: 75])。他所谈到的呼吁涉及我们对人类计算的哪些特征是_基本_特征的理解(一些_非_基本特征的例子是人类计算机吃饭、呼吸和睡觉)。

概括地说,论证 I 的论点如下:鉴于人类计算具有_这些_(而且仅仅是这些)基本特征——图灵在这里列出了一系列特征——那么,无论指定了哪种人类计算,都可以设计出一台图灵机来执行计算。因此,图灵机可计算的数字包括所有自然被视为可计算的数字(邱奇的论题)。

4.3.1 图灵的分析

图灵对人类计算的基本特征的列表如下(Turing 1936 [2004: 75–76]):

计算机在二维纸张上写符号,这些纸张可以被认为(或实际上被认为)被划分成方块,每个方块中最多包含一个单独的符号。

  1. 计算机无法识别或打印超过有限数量的不同类型的个别符号。

  2. 计算机无法一次观察无限数量的方块 —— 如果他或她希望观察的方块多于一次可以观察的数量,则必须进行连续的观察。(假设计算机一次可以观察的方块的最大数量为 B,其中 B 是某个正整数。)

  3. 当计算机进行新的观察以查看更多方块时,新观察到的方块中没有一个会离最近先前观察到的方块超过一定的固定距离。(假设这个固定距离由 L 个方块组成,其中 L 是某个正整数。)

  4. 为了改变一个符号(例如,用另一个符号替换它),计算机需要实际观察包含该符号的方块。

  5. 任何时刻计算机的行为是由他或她所观察到的符号和他或她当时的“心态”决定的。此外,计算机在任何给定时刻的心态,连同他或她在那时观察到的符号,决定了计算机在下一时刻的心态。

  6. 当描述计算机行为时需要考虑的心态状态数量是有限的。

  7. 计算机执行的操作可以分解为基本操作。这些操作非常简单,以至于在单个基本操作中不会更改一个以上的符号。

  8. All elementary operations are of one or other of the following forms: 9. 所有基本操作都是以下形式之一:

  9. 一种心态的改变。

  10. 观察到的方块的变化,以及心态的可能变化。

  11. 一个符号的改变,连同可能的心态转变。

4.3.2 下一步:B-L 型图灵机

论证 I 的下一步是要证明,如果人类计算具有那些且仅具有那些基本特征,那么,无论人类计算被指定为什么,都可以设计出图灵机来执行计算。为了证明这一点,图灵引入了一种修改过的图灵机形式,可以称为“B-L 型”图灵机。B-L 型图灵机与普通图灵机有许多共同之处:

  1. 一个 B-L 型图灵机由扫描器和一维纸带组成;纸带被分成方块。

  2. 扫描仪包含使其能够将磁带向左或向右移动的机制。

  3. 扫描仪的机制还使其能够识别、删除和打印符号。

  4. 扫描仪只能识别和打印有限数量的不同类型的个别符号。

  5. 在任何时刻,扫描仪的控制机制将处于有限数量的内部状态之一。图灵将这些称为“m-配置”。他在一份总结中用法语解释了“可计算数”中心思想:“在机器内部,‘杠杆、轮子等可以以几种方式排列,称为‘m-配置’”。(完整摘要见 Copeland & Fan 2022。)

  6. 任何时刻机器的行为是由其 m-配置和它正在观察(即扫描)的符号决定的。

  7. 机器的可能行为受限于移动磁带、删除所观察方格上的符号,以及在所观察方格上打印符号。这些行为中的每一个可能伴随着对 m-配置的改变。

现在转向普通图灵机和 B-L 类型机之间的区别:

  1. 一台 B-L 型机器的扫描器可以一次观察多达 B 个方块;而一般图灵机的扫描器一次只能观察磁带上的一个方块。能够像这样同时调查一系列方块的图灵机有时被称为“串机”(也许不太优雅)。

  2. 一台 B-L 型机器的扫描器可以在一次操作中将磁带一次移动多达 L 个方块(向左或向右移动到任何一个立即前面观察到的方块的位置);而普通机器的扫描器只能在单个基本操作中将磁带移动一个方块。

回到论点,图灵断言,鉴于他对人类计算的基本特征 1-9 的描述,一种 B-L 型机器可以“完成”任何人类计算的工作(1936 年:77)。这是因为 B-L 型机器要么复制要么模拟 特征 1-9 中的每一个。让我们依次看看这些特征。

特征 1 是由机器模拟的:B-L 型机器使用其一维纸带来模仿计算机的二维纸张。邱奇说:

我认为大家会同意,纸张的二维特性并不是计算的本质。(Turing 1936 [2004: 75])

然而,一些评论家指出,在这个问题上存在疑虑的余地。Gandy 抱怨图灵在这里的论证“过于简略”,称:

这并不是完全明显的,计算在二维(或三维)中进行,可以放在一维磁带上,同时保留“局部”属性。(Gandy 1988: 81, 82–83)

德肖维茨和古列维奇问道:

邱奇-图灵论题:在计算过程中使用的每个复杂数据结构都可以被编码为一个字符串,并且其操作可以通过有效的字符串操作模拟,这一点有多确定?(Dershowitz & Gurevich 2008: 305)

继续讨论图灵清单上的其他特征:2、3、4 和 5 在机器中直接复制。特征 6 和 7 通过让机器的 m-配置代表计算机的心智状态来模拟(稍后详细介绍)。特征 8 在机器中复制:机器的复杂操作(如长乘法和除法)是由基本操作构建而成。特征 9 再次通过让 m-配置代表人类心智状态来模拟。

4.3.3 最后一步

下一个也是最后一个论证步骤涉及到的陈述是,任何由 B-L 型机器执行的计算也可以由普通图灵机执行。这是直接的,因为通过一系列单方格移动,普通机器可以模拟 B-L 型机器一次最多 L 个方格的磁带移动;而且普通机器也可以通过一系列单方格扫描(必要时夹杂着 m-配置的更改)模拟 B-L 型机器一次最多 B 个方格的扫描。因此,如果 B-L 型机器可以“完成”人类计算机的工作,普通图灵机也可以。

总之,邱奇已经表明了以下内容——假设他的主张被接受,“计算机的每个心智状态对应于机器的‘m-配置’”:根据上述对人类计算基本特征的描述,一台普通的图灵机能够完成任何人类计算的工作。换句话说:在那个条件和前提下,他已经证实了他的论点,即普通图灵机可计算的数字包括所有自然被视为可计算的数字。

4.3.4 心灵状态,和论证 III

但是,关于邱奇对心灵状态和 m-配置之间的对应的说法应该被接受吗?人类的心灵状态难道不可能远远超越杠杆和轮子的排列吗?计算机的心灵状态难道不可能有时会促使他或她以一种 B-L 型机器无法做到的方式改变符号吗?

图灵在他的补充论证 III 中解决了关于心智状态和 m-配置之间对应的担忧,他说这可以被视为 I 的修改(1936: 79)。在这里,他认为可以完全避免提及计算机的心智状态,而是谈论他所称的“指令笔记”。他说,指令笔记是心智状态的“更明确和物理的对应物”。人类计算的每一步都可以被视为由指令笔记控制 —— 通过遵循笔记中的指令,计算机将知道在该步骤中执行什么操作(擦除、打印或移动)。图灵设想计算机在计算进行过程中即时准备新的笔记:“指令笔记必须使他(计算机)能够执行一步并写下下一个笔记”。每个笔记实际上是一个微型计算机程序,既执行计算的单个步骤,又编写下一个步骤要使用的程序。

一旦指令笔记出现在画面中,就不需要再提及人类计算机的心态状态

在任何阶段,计算的进展状态完全由指令笔记和磁带上的符号决定。(Turing 1936 [2004: 79])

另一种相关的回答担忧的方式是,人类心灵状态可能超越机器的 m-配置,即使这是真的,也不会对论证 I 造成本质上的影响。这是因为 feature 3feature 7(Section 4.3.1):需要考虑的心灵状态数量是有限的,计算机在任一时刻能观察的最大方块数为 B(有限数量)。

鉴于 feature 7,可以得出无论一个心智状态有多复杂,计算机在该心智状态下的相关行为都可以通过有限表格来封装。表格的每一行将采取以下形式:如果观察到的符号是这样,那么执行这样的基本操作(其中基本操作如 feature 9 中所指定)。由于只考虑有限数量的心智状态(feature 3)—假设为 n—关于计算机心智状态的所有必要信息都可以封装在 n 个这样的表格列表中。这个列表由有限多个符号组成,因此可以事先放置在 B-L 型机器的磁带上,然后机器开始模拟人类计算机。(这类似于在通用图灵机的磁带上编写程序。)B-L 型机器在计算的每一步都会查阅列表,机器在每一步的行为完全由列表和当前观察到的符号决定。

总之:无论人类计算机的思维状态被赋予了什么样的能力,只要需要考虑的思维状态是有限的(当然,前提是图灵对计算的基本特征的描述是正确的),那么一台 B-L 型机器仍然可以“完成”计算机的工作。

4.3.5 图灵的定理

现在,既然上面提到的关于心灵状态的限定已经被清除了,图灵在论证 I 中的成就可以总结如下:他已经像甘迪所说的那样,“概述了一个定理的证明”(Gandy 1980: 124)。

图灵的计算定理

这一对人类计算基本特征的描述暗示了邱奇-图灵论题。

现在应该完全清楚为什么图灵称论证 I 为“直接对直觉的呼吁”。如果一个人的直觉告诉他图灵对人类计算的基本特征的描述是正确的,那么定理就可以被应用,图灵的论题就得到了保证。

然而,邱奇的观点并非免疫怀疑。一些怀疑的问题是:图灵是否忽视了人类计算的某些方面?一个受到 1-9 限制的计算机是否无法执行一些人类计算机可以完成的计算?此外,在描述计算机行为时,是否总是需要考虑的心态状态数量必须是有限的?哥德尔认为图灵的“可区分心态状态”的数量可能“趋近于无穷”,称

图灵完全忽视的是,心智在使用中并非静止不变,而是不断发展。 (邱奇 1972: 306)

确实,认为 1-9 是真实的根据应该是什么?这些说法应该建立在人类感官和人类思维的本质和局限性上吗?还是它们应该以其他方式作为基础,例如,以_有效方法_的基本本质作为基础?

图灵的论证 I 是一座高耸的地标,现在已经有大量关于这些问题以及其他相关问题的文献。有关这一重要论点的更多信息,请参阅 Sieg 1994, 2008; Shagrir 2006; 以及 Copeland & Shagrir 2013。

4.4 图灵的论证 II

4.4.1 在逻辑中计算

Kleene 在他对邱奇-图灵论题证据的调查中,列举了一种基于符号逻辑的论证类型(Kleene 1952: 322–3)。 (他将这些类别称为“D”论证。)这类论证以引入一种可能的替代方法来表征有效可计算函数(或者在图灵的情况下,可计算函数或数字)为开端。这种替代方法涉及到某种符号逻辑中的可导性:有效可计算性(或可计算性)的概念是以_逻辑内的可计算性_来表征的(见 Section 3.3)。按照概要,这种表征形式是:如果函数的每个连续值在逻辑中是可导的,那么该函数就是有效可计算的(或可计算的)。然后,论证的下一步是建立新的表征(无论是什么)与旧表征等价。在邱奇的情况下,这相当于论证新的表征等价于他以递归性或 λ-可定义性来表征的。最后,声称新的和以前的表征是等价的结论被视为支持邱奇-图灵论题的进一步证据。

在他的调查中,Kleene 通过描述 Church 的论证(Church 1936a: 357–358)来阐明这种方法。 图灵的论证 II 也是这种类型,但奇怪的是,Kleene 没有提到它(尽管他在 1952 年的调查中分配了五页给图灵的论证 I)。

4.4.2 邱奇的“逐步”论证

这是一个有启发性的研究教堂的论证——被甘迪称为“逐步”论证(Gandy 1988: 77)——在考虑图灵的 II 之前。教堂引入了以下替代方法,并将其描述为与定义有效可计算性相关的“自然建议的方法”之一。

一个正整数的函数 F 被定义为有效可计算的,如果对于每个正整数 m,存在一个正整数 n,使得 F(m)=n 是一个可证明的定理。(Church 1936a: 358)

Church 没有指定任何特定的符号逻辑。他只规定了逻辑必须满足的一些一般条件(1936a: 357)。这些条件包括逻辑的公理列表必须是有限的或可枚举无限的,并且逻辑的每条规则必须指定一个“有效可计算操作”(他说,如果逻辑“要起到符号逻辑系统通常预期的所有目的,这是必要的”)。引入了这种替代方法来描述有效可计算性后,Church 接着论证说,以这种方式在逻辑中“可计算”的每个函数(一个正整数)也是递归的。他得出结论,支持 Church 的论点,即新方法产生的“对于有效可计算性没有比提出的更一般的定义”,即递归性(1936a: 358)。

4.4.3 图灵的变体

图灵在对第二论证的前言中指出了它与邱奇论证的广泛相似之处。图灵将第二论证描述为一种“两个定义等价的证明”,并补充说:“如果新定义更具直观吸引力的话”(1936 年[2004: 75])。

图灵的论证与邱奇的不同,涉及到一个特定的符号逻辑,即希尔伯特的一阶谓词演算。第二论点依赖于一个可以称为

图灵的可证性定理

每个可在希尔伯特一阶谓词演算中证明的公式都可以被通用图灵机证明。(见邱奇 1936 [2004: 77]。)

邱奇-图灵论题中考虑的另一种方法(类似于邱奇的方法)是用各种陈述来表征一个可计算数(或序列),其中每个陈述都提供该数(或序列)的下一个数字。如果在希尔伯特的演算中每个这样的陈述都是可证的(其想法是,如果是这样,那么希尔伯特的演算可以用来逐个计算或推算出该数的数字),则称该数(序列)是可计算的。图灵利用可证性定理,随后证明了以下内容:根据这一替代定义,每个可计算的数也符合图灵机的定义(即,该数的数字可以逐步被图灵机写出),反之亦然(图灵 1936 年[2004:78])。换句话说,他证明了这两种定义的等价性,如他所承诺的那样。

4.4.4 比较邱奇和图灵论证

回到邱奇的逐步论证,这里有些诡计。邱奇希望得出结论,即“在逻辑范围内可计算的”函数是递归的,并且在为此进行论证的过程中,他发现有必要断言逻辑的每条规则都是一个递归操作,因为每条规则都要求是一个有效可计算的操作。在不同的背景下,他可能会通过诉诸邱奇-图灵论题来支持这一断言(毕竟邱奇-图灵论题说,有效可计算的东西是递归的)。但在当前背景下,这样的诉诸自然是先入为主的。

邱奇也没有提出这样的呼吁。(Sieg 描述邱奇的推理为“半圆形”,但这似乎太苛刻了——这并没有什么循环;Sieg 1994: 87, 2002: 394。)但邱奇也没有提出任何有力的理由来支持他的断言。他只是举了一些规则是递归操作的系统的例子;并且还说——在规定了每个程序规则必须是可有效计算的操作之后——他将“_解释为_每个程序规则必须是递归操作”(1936: 357,斜体添加)。简而言之,邱奇论题的邱奇论证的一个关键步骤得到了不充分的支持。Sieg 著名地将这一步骤称为邱奇论证中的“绊脚石”(Sieg 1994: 87)。

在邱奇的论证中并不存在这样的困难。在选择了特定的逻辑(希尔伯特的演算)之后,邱奇能够指定一台“找到该演算中所有可证公式”的图灵机,从而毫无疑问地表明在该逻辑中可计算的函数是图灵机可计算的(邱奇 1936 年[2004: 77])。因此,邱奇的第二论证更胜于教会的逐步论证。

4.5 克里普克对论证 II 的版本

最近对这一领域的重要贡献是由 Kripke(2013)做出的。对于邱奇-图灵论题的传统观点是,虽然已经积累了“相当可观的直觉证据”,但这个命题“并不足够精确,无法被数学方法处理”(Kripke 2013: 77)。Kleene 早期表达了这一现在被普遍接受的观点:

自从我们对函数的有效可计算性的最初概念...是一个有些模糊的直观概念,这个论题无法被证明...虽然我们无法证明邱奇的论题,因为它的作用是精确界定一个此前模糊构想的整体,我们需要证据...(Kleene 1952: 318)

拒绝传统观点,克里普克(Kripke)提出,相反,邱奇-图灵论题(Church-Turing Thesis)容易受到数学证明的影响。此外,他探讨了图灵本人勾勒出的一种论证,可以证明这个命题。

Kripke 试图围绕图灵的论证 II 建立邱奇-图灵论题的数学论证。他声称他的论证“非常接近”图灵的(Kripke 2013: 80)。然而,这是值得商榷的,因为在细节上,Kripke 的论证与论证 II 有相当大的不同。但至少可以说,Kripke 的论证是受到图灵的论证 II 的启发,并且属于 Kleene 的“D”类别(与 II 和 Church 的逐步论证一起)。

Kripke 认为邱奇-图灵论题是戈德尔关于带有恒等性的一阶谓词演算的完备性定理的一个推论。用比较粗糙的话说,后者定理陈述了每个在带有恒等性的一阶谓词演算语言中陈述的有效演绎都可以在演算中被证明。换句话说,从前提 A1,A2,…An(其中陈述 A1,A2,…An,B 都在带有恒等性的一阶谓词演算语言中)推导出 B 的推理在逻辑上是有效的当且仅当 B 可以在演算中从 A1,A2,…An 被证明。

Kripke 论证的第一步是他声称(无误差的人类)计算本身就是一种推理形式

[一个] 计算是数学论证的一种特殊形式。给定一组指令,计算中的步骤应该——根据给定的指令——推导出来。因此,计算只是另一种数学推导,尽管是一种非常专门化的形式。 (Kripke 2013: 80)

以下伪代码中的两行程序说明了克里普克的观点。符号“→”读作“变为”,而“=”通常表示相等。程序中的第一条指令是 r→2。这告诉计算机将值 2 放入存储位置 r (假定最初为空)。第二条指令 r→r+3 告诉计算机将 3 添加到 r 的内容中,并将结果存储在 r 中(覆盖 r 的先前内容)。这个两行程序的执行可以表示为一个推导:

{执行 r→2,紧接着执行 r→r+3} 逻辑上意味着在随后的状态中 r=5。

在邱奇-图灵论题中,邱奇为表达所有这类推导开发了详细的逻辑符号(Turing 1936)。

(事实上,_任何_一系列指令的成功执行都可以用这种方式演绎地表示——克里普克并没有注意到计算特有的特征。这些指令不需要是计算机可以执行的指令。)

Kripke 论证的第二步是诉诸他所称的_希尔伯特论题_:这个论题是任何数学论证的步骤可以用“基于一阶逻辑(带有恒等性)的语言来表达”(Kripke 2013: 81)。称这一主张为“希尔伯特论题”的做法起源于 Barwise(1977: 41),但应注意,由于希尔伯特认为二阶逻辑是不可或缺的(参见,例如,Hilbert&Ackermann 1928: 86),因此“希尔伯特论题”的名称可能具有误导性。

将“希尔伯特的论题”应用于克里普克上述声称的“计算只是另一种数学推导”(2013: 80)得到:

每一个(人类)计算都可以被形式化为一种有效的推导,用一阶谓词演算与恒等性的语言来表达。

现在,将哥德尔的完备性定理应用于这一点,依次产生:

每个(人类)计算都可以用带有恒等性的一阶谓词演算来证明,这意味着,给定适当的形式化,计算的每一步都可以从指令中推导出来(可能与辅助前提一起,例如,众所周知的数学前提,或者在计算开始时提供给计算机的有关数字的前提)。

最后,将图灵的可证性定理应用于这个中间结论,得出邱奇-图灵论题:

每一个(人类)计算都可以由图灵机完成。

4.6 邱奇-图灵论题的地位

正如 第 3.4 节 所提到的,德肖维茨和古列维奇也认为邱奇-图灵论题容易受到数学证明的影响(Dershowitz & Gurevich 2008)。他们提出“对邱奇论题的证明,正如哥德尔和其他人所建议的可能性”(2008: 299),并补充说:

以类似的方式,但使用不同的基本操作集,可以证明图灵的论题,...。 (Dershowitz & Gurevich 2008: 299)

然而,图灵本人对他的论题地位的看法与克里普克、德肖维茨和古列维奇所表达的看法大不相同。根据图灵,他的论题不容易受到数学证明。他并未认为论证 I 或论证 II 是他论题的数学证明:他断言 I 和 II,以及“[a]ll arguments which can be given”(所有可能提出的论证)都不是他的论题的数学证明。

基本上, 对直觉的呼吁, 因此在数学上相当不令人满意。 (Turing 1936 [2004: 74])

的确,邱奇可能认为“希尔伯特论题”本身就是一个只能通过直觉来证明的命题的例子。

图灵讨论了与图灵论题密切相关的一个命题,即_对于每种系统方法,都有一个相应的替换谜题_(其中“替换谜题”,就像“可由图灵机计算”,是一个严格定义的概念)。他说:

这个陈述是……一个人不尝试证明的陈述。宣传比证明更适合它,因为它的地位介于定理和定义之间。(Turing 1954 [2004: 588])

也许图灵会认为这种说法同样适用于邱奇-图灵论题,即_对于每种系统方法,都有一个相应的图灵机_。

图灵还说(在 2004 年出版的手稿中),“系统方法”这个短语

是一个短语,就像许多其他短语(例如,“蔬菜”)一样,在日常生活中人们都能理解得很好。但是当与蔬菜商、微生物学家交谈或玩“二十个问题”时可能会遇到困难。大黄和番茄是蔬菜还是水果?煤是蔬菜还是矿物?煤气、骨髓、化石树、链球菌、病毒呢?我午餐吃的生菜已经变成动物了吗?…关于上述问题 c)[我是否有一种系统方法可以回答这类问题]也会出现同样的困难。对“系统方法”这个短语的普通了解是不够的,因为人们必须能够非常清楚地表明对于任何可能被提出的方法,它是否是允许的。 (邱奇-图灵论题中的图灵,Copeland 2004: 590)

在这里,图灵强调“系统方法”这个术语并不精确,因此在这方面类似于“蔬菜”这个术语,不同于数学上精确的术语,如“λ-可定义”、“图灵机可计算”和“替换拼图”。Kleene 声称,由于诸如“系统方法”和“有效可计算”之类的术语并不精确,涉及它们的论题无法被证明。然而,图灵并没有提出类似的论点(也许是因为他看到了困难)。“系统方法”这个术语不精确_并不足以表明_不存在涉及该术语的论题的数学上可接受的证明。Mendelson 对这一观点进行了生动阐述,写到了上文所称的“邱奇-图灵论题的逆”(1.5 节)。

假设连接直觉和精确数学概念的证明是不可能的这一假设显然是错误的。事实上,邱奇-图灵论题的一半(“更容易”的一半),即所有部分递归函数都是有效可计算的这一断言,被公认为在递归理论的所有教科书中都是显而易见的。可以为此提供一个直接的论证……这个简单的论证就像我在数学中见过的证明一样清晰,尽管它涉及到有效可计算性的直观概念。(Mendelson 1990: 232–233)

然而,“直觉”性质的一些术语并不排除该论题是可证明的这一观点,并不意味着该论题是可证明的。如果邱奇-图灵论题的地位是“介于定理和定义之间的某种东西”,那么定义很可能是邱奇提出的“定义……有效可计算函数的概念”(第 1.5 节),而定理则是图灵的计算定理(第 4.3.5 节),即,鉴于图灵对人类计算的基本特征的阐述,图灵的论题是正确的。这个定理是可以证明的,但要从定理证明论题本身,则需要用数学确定性地展示图灵对人类计算基本特征的阐述是正确的。到目前为止,还没有人做到这一点。宣传似乎比证明更为合适。

5. 邱奇-图灵论题和机器的局限

5.1 两个不同的命题

能够完美模拟_每一台_机器的行为吗?邱奇-图灵论题有时被视为对机械的逻辑限制提供了一种说明,即通用图灵机是可能的最一般的机器(因此,对刚提出的问题的答案是_是_)。例如:

存在一种最一般的机器形式,并且它导致一组唯一的输入-输出函数的观点被称为邱奇-图灵论题。 (Newell 1980: 150)

然而,邱奇-图灵论题是关于_有效_方法的论题(其中蕴含着它的数学重要性)。换句话说,这个论题涉及到一个_人类_在通过死记硬背、使用纸和铅笔进行计算时可以实现什么(假设没有无聊、死亡或纸张不足等情况)。一个人类死记硬背者可以实现的,以及一台机器可以实现的,可能是不同的。

Gandy 可能是第一个明确区分图灵论题和非常不同命题的人,即_任何可以由机器计算的东西都可以由图灵机计算_(Gandy 1980)。Gandy 将这个命题称为“M 命题”。他指出,在一些“遵循牛顿力学的机器”中,事实上 M 命题是错误的,那里“可能有任意长度的刚性杆和以任意大速度行进的信使”(1980: 145)。他还指出,M 命题不适用于他所称的“本质上是模拟机器”(1980: 125)。一个非常有趣的问题是 M 命题是否适用于所有与_实际物理定律_一致的_离散_(即非模拟)机器。这个问题在 第 6.4 节 中讨论。

邱奇-图灵论题 M 不够精确,因为甘迪从未明确指出他所说的“由机器计算”。陈述一个更明确的命题来捕捉邱奇-图灵论题 M 的精神是很有用的。这可能被称为_强邱奇-图灵论题_,但总的来说,避免使用那个名字似乎更可取,因为所讨论的命题与 1936 年的邱奇-图灵论题非常不同。这个命题将被称为“极大性命题”。

一些更多的术语:如果一台机器_m_能够被设置成这样,即当_m_被提供函数的任何参数(例如 4)时,m_将执行一系列处理步骤,最终产生函数对应的值(例如例子中的 16),那么将说机器_m_会_生成(从图灵 1937 年借用此词)某个函数(例如_x_的平方)。对于像加法这样需要多个参数的函数,mutatis mutandis

最大性论题

所有可以由机器生成的函数都是有效可计算的。

“Effectively computable”是一个常用术语:如果(且仅如果)存在一种有效方法来获得其值,则称函数是有效可计算的。用有效可计算性来表达,邱奇-图灵论题说:所有有效可计算的函数都是图灵机可计算的。

显然,邱奇-图灵论题和最大性论题是不同的命题。

5.2 “等价谬误”

一个支持最大性论题或等价命题的常见论据是指出上面提到的事实,即许多不同的尝试以精确的术语分析可计算性的非正式概念——由图灵、邱奇、Post、马尔可夫和其他人尝试——结果证明彼此_等价_,即每个分析都可以证明地确定出相同的函数类,即图灵机可计算的函数。

正如前面提到的,这些分析的融合通常被认为是邱奇-图灵论题的有力证据(这是该论题的等价论证—Section 4.1)。有些人进一步认为,这种融合也证明了最大性论题。例如,纽厄尔(Newell)提出,邱奇、图灵、波斯特(Post)、马尔可夫(Markov)等人给出的分析的融合表明

所有尝试去制定一般性的机制概念都会导致等效的机器类别,因为它们完全包含着相同的输入-输出函数集合。 (Newell 1980: 150)

各种等效分析,据纽厄尔说,构成了一

大量不同形式的机器最大类的动物园。 (同上)

或许这里存在一个谬误。Newell 正在讨论的分析是关于有效方法的概念:这些分析的等价性仅涉及到人类可计算的范围,而不涉及一个更深层次的问题,即机器生成的函数是否可能超出原则上可人类计算的范围。

5.3 观察我们的言辞

这时候可能有必要调查一些标准的技术术语,这些术语可能会对不谨慎的人构成陷阱。

5.3.1 可计算的一词

正如已经强调的那样,当图灵谈论可计算数时,他谈论的是人类可计算的数。他说:“通常是通过在纸上写入某些符号来进行计算”(1936 年[2004: 75])——通常是“通过人类文书劳动,按照固定规则工作”(1945 年[2005: 386])。他说,“计算机”可能会“以一种如此散漫的方式进行,以至于他一次永远不会做多于一步”(1936 年[2004: 79])。人类计算机的工作是可机械化的:“我们现在可以构造一台机器” —— 图灵机 —— “来代替这台计算机的工作”(1936 年[2004: 77])。有关这一关键点的更多引文,请参见 第 7 节

因此,“On Computable Numbers”中的各种结果,即某些函数是不可计算的,因此涉及人类计算机。图灵不应被解释为意在陈述有关机械限制的结果。 甘迪写道:

这绝非显而易见,[第 4.3 节 上述]中描述的限制是否适用于机械设备;邱奇并未声称如此。(Gandy 1988: 84)

5.3.2 两个启示性的引文

某些函数在绝对意义上是不可计算的:即使是[图灵机]也无法计算,因此也无法被任何过去、现在或未来的真实机器计算。(Boolos & Jeffrey 1974: 55)

在技术逻辑文献中,“可计算”一词通常用来表示“有效计算”(尽管并非总是如此—请参阅 5.3.3 节)。(“有效计算”在 5.1 节 中有定义。)由于 Boolos 和 Jeffrey 使用“可计算”来表示“有效计算”,他们在这段引文中所说的实质是,所讨论的函数_不能_被任何过去、现在或未来的真实机器有效计算—这是正确的,因为根据假设,这些函数_不_是有效计算的。然而,对于文献的普通读者来说,这种表述(以及类似的其他表述)可能会显得比实际情况更具含义。一个函数是_不可计算_的(即有效地不可计算),不意味着该函数不能_被某台真实机器生成_,无论是过去的、现在的还是未来的。

第二引语:

形式机器行为的限制...存在某些“不可计算”的行为-对于这些行为,无法为将展示该行为的机器提供形式规范。这种限制的经典例子是图灵著名的停机问题:我们能否为一台机器提供形式规范,当提供另一台机器的描述及其初始状态时,将确定该机器是否会达到其停机状态?图灵证明了无法指定这样的机器。(Langton 1989: 12)

被证明的是,没有任何_图灵机_能够始终确定,当提供了_任何_图灵机的描述以及其初始状态时,该机器是否会达到其停机状态。邱奇确实证明了没有任何东西表明不可能指定一种_某种类型的_机器来做朗顿描述的事情。因此,朗顿提出的考虑并没有对机器行为施加任何一般形式的限制,只是对图灵机的行为。然而,这段引文给人另一种印象。(顺便说一句,值得指出的是,尽管停机问题通常被归因于图灵,就像朗顿在这里所做的那样,但事实上图灵并没有提出它。停机问题起源于 1950 年代初的戴维斯(Davis 1958: 70)。)

5.3.3 超越有效

一些作者使用诸如“广义计算”或简单地“计算”等短语来指代一种可能超越有效计算的计算类型(例如,Doyle 2002;MacLennan 2003;Shagrir & Pitowsky 2003;Siegelmann 2003;Andréka, Németi, & Németi 2009;Copeland & Shagrir 2019)。

Doyle, 例如, 暗示说具有离散光谱的_平衡系统_(例如,分子或其他量子多体系统)可能展示了一个比有效计算更广泛的计算概念。由于“平衡可以如此轻松、可靠且毫不费力地完成”,Doyle 说,我们可以将“平衡的操作”视为一种计算操作,即使在原则上使用图灵机操作_加上_平衡的函数中包括一些无法通过单独的图灵机计算的函数(Doyle 2002: 519)。

5.3.4 机械这个词

在“机械”的技术文献中和日常含义之间存在着天壤之别。“机械”和“有效”通常可以互换使用:一个“机械”的程序就是一个有效的程序。Gandy 1988 概述了这个词“机械”被使用的历史。

在文献中会出现类似以下的陈述:

图灵提出,一定类别的抽象机器【图灵机】可以执行任何“机械”计算过程。(Mendelson 1964: 229)

这可能被误解为邱奇-图灵论题 M。然而,“mechanical”在这里是以其技术意义使用的,该声明仅仅是邱奇-图灵论题:

图灵提出,一定类别的抽象机器可以执行任何有效的计算程序。

“机械”一词的技术用法往往会模糊概念上的可能性,即并非所有机器可生成的函数都是图灵机可计算的。问题“_机器_能否实现非机械的程序?”可能看似自问自答——然而,如果质疑邱奇-图灵论题和极大性论题,这就是所问之事。

5.4 强大极大论题

最大性论题有两种解释,取决于短语“可以由机器生成”是以“可以由符合实际世界物理定律的机器生成”(论题的弱形式)的意义,还是以量化所有机器为对象,而不考虑是否符合实际物理定律(论题的强形式)。 (强弱术语反映了强形式蕴含弱形式,但反之则不然。)

弱形式将在 第 6.4 节 中讨论。已知强形式是错误的。这可以通过提供一个例子来展示,即一个虚构的机器能够生成一个无法有效计算的函数。这里将提供一个例子;更多例子可以在 Andréka 等人的 2009 年、Davies 的 2001 年、Hogarth 的 1994 年、Pitowsky 的 1990 年、Siegelmann 的 2003 年以及下面提到的其他论文中找到。

5.4.1 加速图灵机

加速图灵机(ATMs)与标准图灵机完全相同,只是它们的运行速度会随着计算的进行而加快(Stewart 1991;Copeland 1998a,b,2002a;Copeland&Shagrir 2011)。ATM 执行其程序要求的第二个操作所用时间是执行第一个操作的一半,执行第三个操作所用时间是执行第二个操作的一半,依此类推。

如果执行第一个操作所需的时间被称为一个“瞬间”,那么第二个操作在半个瞬间内完成,第三个操作在四分之一瞬间内完成,依此类推。自邱奇-图灵论题

12+14+18+…+12n+12n+1+…≤1,

一个 ATM 能在两个操作时间内执行无限多的操作。这使得 ATM 能够生成任何标准图灵机无法计算的函数(因此,根据邱奇-图灵论题,这些函数并非有效可计算的)。

一个这样函数的例子是_停机函数 h_。如果第 n 个图灵机停机,则 h(n)=1;如果第 n 个图灵机无休止地运行,则 h(n)=0。众所周知,没有标准图灵机能够计算这个函数(邱奇-图灵论题 1958);但是一个 ATM 可以在有限时间内产生函数的任何值。

在计算 h(n) 时,ATM 的第一步是在一块被称为答案方块(A)的磁带上写下“0”。然后,ATM 继续模拟第 n 台图灵机的操作。如果 ATM 发现第 n 台机器停机,那么 ATM 将擦除先前写在 A 上的“0”,将其替换为“1”。另一方面,如果第 n 台机器没有停机,ATM 将永远不会返回到方块 A 上擦除最初写在那里的“0”。无论哪种方式,一旦经过两个操作时间,A 中就包含了值 h(n)(Copeland 1998a)。

这个概念机器是对强大最大性论题的反例。

6. 邱奇-图灵论题的现代版本

6.1 算法版本

在现代计算机科学中,算法和有效程序主要与机器相关联,而不是与人类相关联。因此,许多计算机科学教科书在阐述邱奇-图灵论题时,并未提及人类计算机(例如,Hopcroft & Ullman 1979;Lewis & Papadimitriou 1981)。尽管人类计算的概念是图灵和邱奇分析的核心,但这一事实仍然存在。

现代计算机科学研究的算法种类比图灵时代的领域更加广泛。现在有并行算法、分布式算法、交互式算法、模拟算法、混合算法、量子算法、酶算法、细菌觅食算法、粘菌算法等等(参见例如,Gurevich 2012; Copeland & Shagrir 2019)。通用图灵机甚至无法执行诸如并行系统中每个单元同时更新(与串行图灵机相反)或酶系统(其中原子步骤涉及选择性酶结合)等算法的原子步骤。

然而,通用图灵机仍然能够_计算_并行系统和酶系统的行为。邱奇-图灵论题的算法版本陈述了这对_每个_算法系统都成立。因此,Lewis 和 Papadimitriou 说:“我们认为图灵机是‘算法’直观概念的精确形式等价物”(1981: 223)。David Harel 给出了以下(著名的)算法版本论题的表述:

任何我们可以找到一个算法,并且可以用某种编程语言,_任何_语言编程的算法问题...也可以被图灵机解决。这个说法是所谓的邱奇-图灵论题的一个版本。(Harel 1992: 233)

鉴于自 1930 年代以来算法概念的演变程度——从人类计算机的逐步劳动到粘菌的增长——引发了一些有趣的问题。这个概念会继续演变吗?这种演变有哪些限制,如果有的话?这个概念是否会演变到某种程度,以至于邱奇-图灵论题的算法版本不再普遍成立?回到道尔关于平衡系统的建议(见 5.3.3 节),道尔的主张基本上是,平衡操作可以合理地被视为某些有效程序或算法的基本步骤——_无论_最终的算法是否符合邱奇-图灵论题的算法版本。(有关进一步讨论,请参阅 Copeland&Shagrir 2019。)

总之,邱奇-图灵论题的算法版本比原始论题更广泛,因为邱奇和图灵基本上只考虑了一种类型的算法,即纸上的有效逐步计算。算法版本也可能比原始论题不太可靠。

6.2 计算复杂性:扩展的邱奇-图灵论题

邱奇-图灵论题现在不仅在可计算性理论中占据中心地位,而且在复杂性理论中也占据中心地位。量子计算研究者 Bernstein 和 Vazirani 说:

正如可计算性理论以邱奇-图灵论题为基础一样,计算复杂性理论则建立在对这一论题的现代加强基础之上。(Bernstein & Vazirani 1997: 1411)

事实上,在现代计算机科学文献中,实际上存在两个不同的复杂性理论版本的邱奇-图灵论题。两者都被称为“扩展的邱奇-图灵论题”。第一个是由姚期智在 2003 年提出的:

邱奇-图灵论题(ECT)提出了这样的断言:图灵机模型在效率上也与任何计算设备一样高效。也就是说,如果某个函数能够在大小为 n 的输入上由某个硬件设备在时间 T(n)内计算出来,那么它也可以由图灵机在时间(T(n))k 内计算出来,其中 k 是某个固定值(取决于问题)。(Yao 2003: 100–101)

姚指出,邱奇-图灵论题有一个强大的含义:

至少原则上,要使未来的计算机更加高效,只需要专注于改进当今计算机设计的实现技术。 (2003: 101)

与原始的邱奇-图灵论题(其地位介于定理和定义之间)不同,ECT 既不是逻辑数学定理,也不是定义。如果它是真的,那么它的真实性是物理定律的结果 - 而它可能不是真的。(尽管如果与计算机科学中一个标准但未经证明的假设相反,P = NP,则这是微不足道的。)

第二个与复杂性理论有关的版本涉及到_概率图灵机_(由 Rabin & Scott 1959 提出)。瓦齐拉尼和阿哈罗诺夫陈述了这个论题:

邱奇-图灵论题…断言任何合理的计算模型都可以被经典计算的标准模型高效地模拟,即概率图灵机。(Aharonov & Vazirani 2013: 329)

这两个相关的论题与原始的邱奇-图灵论题有很大不同,其中最重要的是这两个延伸论题都是_经验性_假设。此外,关于量子计算机是否实际上证伪了这些论题仍在进行讨论。(有关这一讨论的介绍,请参阅 Copeland&Shagrir 2019,有关更详细的论述,请参阅 Aharonov&Vazirani 2013。)

6.3 大脑模拟和邱奇-图灵论题

有时候人们说邱奇-图灵论题对计算模拟的范围有着重要意义。例如,Searle 写道:

大脑的运作能在数字计算机上模拟吗?……答案似乎是……可以肯定是“是”……也就是说,自然解释,这个问题的意思是:是否存在大脑的某种描述,以便在该描述下,你可以对大脑的运作进行计算模拟。但鉴于邱奇-图灵论题指出,任何可以被准确描述为一组步骤的东西都可以在数字计算机上模拟,因此可以轻易得出这个问题肯定的答案。(Searle 1992: 200)

另一个例子:

我们可以依赖于存在一台捕捉大脑功能关系的图灵机

邱奇-图灵论题

这些输入和输出之间的关系在功能上表现良好,足以用数学关系描述...我们知道某个特定版本的图灵机将能够模仿它们。(Guttenplan 1994: 595)

Andréka, Németi 和 Németi 提出了关于图灵机模拟其他系统能力的更一般性论题:

邱奇-图灵论题 … 是这样的猜想:无论未来的文明设计出什么样的物理计算设备(在更广义上)或物理思想实验,它都可以被图灵机模拟。 (Andréka, Németi, & Németi 2009: 500)

Andréka, Németi 和 Németi 甚至说,他们在这里陈述的论题“是在 1930 年代被提出并广泛接受的”(同上)。

然而,邱奇和图灵在 1930 年代制定的并不是关于物理系统模拟的论题,而是关于人类计算的完全不同的论题—正是后者在 1930 年代和 1940 年代得到了普遍接受。

这样称呼关于模拟的论题为“邱奇论题”或“邱奇-图灵论题”确实会使事情变得更加混乱,因为邱奇和图灵用来支持他们实际论题的论据根本无法支持上述几个引文中阐述的论题。然而,可以称之为“模拟论题”的东西在当前现代邱奇-图灵论题的各种形式目录中有其位置。

模拟论题

任何系统,其操作可以被描述为一组步骤(Searle)或其输入-输出关系可由数学关系描述(Guttenplan),都可以被图灵机模拟。

如果模拟论旨在涵盖所有可能的系统,那么它肯定是错误的,因为多伊尔所设想的均衡系统证伪了它(5.3.3 节)。另一方面,如果这个论题旨在涵盖只有实际物理系统,包括大脑在内,那么模拟论就像扩展的邱奇-图灵论题一样,是一个_经验_论题—因此与图灵的论题和邱奇的论题非常不同。模拟论的“实际物理系统”版本的真实性取决于物理定律。

一个可能的反对意见是,任何支持模拟论题的人都需要面对的一个困难与甘迪为 M 论题提出的困难相似(5.1 节)。不是离散的物理系统,比如甘迪的“本质上是模拟机器”,似乎证伪了模拟论题,因为具有连续动力学的系统的变量将任意实数作为它们的值,而图灵机仅限于_可计算_实数,因此无法完全模拟连续系统。

这将讨论直接转向该领域中最有趣的话题之一,即所谓的“邱奇-图灵论题”的“物理版本”。

6.4 邱奇-图灵论题和物理

6.4.1 德意志-沃尔夫勒姆论题

1985 年,Wolfram 提出了一项他称之为“邱奇-图灵论题的物理形式”的论点:

通用计算机在其计算能力上与任何可以实现的物理系统一样强大,因此它们可以模拟任何物理系统。

德意志(奠定了量子计算基础)在 1985 年独立提出了类似的论题,并将其描述为邱奇-图灵论题的“物理版本”

我现在可以陈述邱奇-图灵论题的物理版本:“每个有限实现的物理系统都可以通过有限手段操作的通用模型计算机完美模拟。” 这种表述既更明确定义,也更具物理性,胜过了图灵自己表达的方式。(Deutsch 1985: 99)

这个论题肯定比图灵的论题“更具物理性”。然而,它与图灵自己的主张完全_不同_,因此将其呈现为图灵所说内容的“更明确定义的”版本可能会引起混淆。正如已经强调的,图灵讨论的是_有效方法_,而德沃斯和沃尔夫拉姆提出的论题涉及所有(有限实现的)物理系统——无论该系统的活动是否有效。

在迪奥茨和沃尔夫拉姆的早期工作之后,“邱奇-图灵论题的物理形式”、“邱奇-图灵论题的物理版本”甚至“_邱奇-图灵论题_的物理版本”这些短语现在在当前文献中相当常见。然而,最好避免使用这些术语,因为这些物理论题与图灵的论题和邱奇的论题非常遥远。

在他 1985 年的论文中,Deutsch 接着指出,如果在他的物理论题中,将“一个通过有限手段运行的通用模型计算机”这个描述替换为“一个通用图灵机”,那么结果:

每个有限实现的物理系统都可以被一台通用图灵机完美模拟

这并不正确。他这样说的理由是在 6.3 节 讨论的重点,涉及非离散物理系统。德沃斯认为通用图灵机“无法完美模拟任何经典动力系统”,因为“由于经典动力学的连续性,经典系统的可能状态必然形成一个连续体”,而通用图灵机是一个离散系统(Deutsch 1985: 100)。德沃斯随后引入了一个重要概念,即通用量子计算机,称(但没有证明)这个计算机“能够完美模拟每一个有限的、可实现的物理系统”(1985: 102)。

以下公式在细节上与沃尔夫拉姆和德意志的论点有所不同,但可以说捕捉到了两者的精神。鉴于德意志-甘迪关于连续系统的观点,完美模拟的概念被替换为模拟_任意所需精度的_概念。

德意志-沃尔夫拉姆论题

每个有限的物理系统都可以被一台通用图灵机模拟到任意指定的精度程度。(Copeland & Shagrir 2019)

相关的物理论题由 Earman 1986,Pour-El 和 Richards 1989,Pitowsky 1990,Blum 等人 1998 等人提出。邱奇-图灵论题与 Gandy 的 M 论题以及弱极大性论题密切相关(第 5.4 节)。事实上,邱奇-图灵论题包含了后者(但反之不成立,因为极大性论题仅涉及_机器_,而邱奇-图灵论题涉及_所有_有限物理系统的行为——尽管任何认为每个有限物理系统都是计算机的人会持不同意见;请参见例如 Pitowsky 1990)。

是否德意志-沃尔夫拉姆论题是真实的?这是一个开放性问题(Copeland&Shagrir 2020)—弱极大性论题也是如此。辩论的焦点之一是,如果存在物理_随机性_,是否会证伪这些论题(Calude 等人 2010;Calude&Svozil 2008;Copeland 2000)。但即使在非随机系统的情况下,至少六十年来一直有人猜测,可能存在真实的物理过程(因此,潜在地,机器操作),其行为既不可计算也不可近似于通用图灵机。例如,参见 Scarpellini 1963,Pour-El 和 Richards 1979,1981,Kreisel 1967,1974,1982,Geroch 和 Hartle 1986,Pitowsky 1990,Stannett 1990,da Costa 和 Doria 1991,1994,Hogarth 1994,Siegelmann 和 Sontag 1994,Copeland 和 Sylvan 1999,Kieu 2004,2006(请参见其他互联网资源),Penrose 1994,2011,2016。

选取一个例子,比如说,从这个列表中选取一篇论文:Pour-El 和 Richards 在他们 1981 年的文章中展示,一个系统根据可计算的初始条件按照熟悉的三维波动方程演化,能够展现出违背了 Deutsch-Wolfram 论点的行为。然而,现在和过去一样,这个问题仍然是一个未决问题,即这些初始条件是否在物理上是可能的。

6.4.2 “Gandy argument”

Gandy (1980) 对是否存在确定性、离散系统的行为无法被通用图灵机计算进行了深入讨论。现在著名的“Gandy 论证”旨在表明,在某些方面,Gandy 论证类似并扩展了图灵的 I 论证,Gandy 认为这是对图灵的 I 的改进和更一般的替代(1980: 145)。他强调(与图灵的论证不同),他的论证考虑了“并行工作”(1980: 124-5);正是这一点导致了 Gandy 的分析相对于图灵的分析更加复杂。

Gandy 视其论证的结论(即每个离散确定性机制的行为都可以通过图灵机计算)为相对 先验,可基于一组非常一般的物理假设(即 第 3.4 节 中提到的四个公理)进行证明。这些假设包括,例如,对机制组成部分维度的下限以及效应和信号传播速度的上限。(该论证旨在仅涵盖遵守相对论原理的机制。)Gandy 通过精确的公理,即他称之为原则 I – IV,集合论地表达了他的各种物理假设。例如,第三原则捕捉了这样一个观念,即机器状态是由有限种基本部件(原子)组装而成的数量受限;而 Gandy 称之为“局部因果关系原则”的第四原则捕捉了这样一个观念,即每个状态转换必须由机制部件的局部环境确定。

Gandy 非常清楚地指出,他的论点不适用于连续系统——他称之为模拟机器——和非相对论系统。(Gandy 的未发表作品摘录在 Copeland&Shagrir 2007 年的著作中,其中他试图为模拟机器发展一个类似的论点。) 但是,Gandy 论点的适用范围在其他方面也有限,这是 Gandy 本人没有注意到的。例如,一些异步算法超出了 Gandy 原则的适用范围(Gurevich 2012; Copeland&Shagrir 2007)。Gurevich 得出结论称,Gandy 并未表明“他的公理被所有离散机械设备满足”,Shagrir 表示没有“依据表明 Gandy 表征了有限机器计算”(Gurevich 2012: 36,Shagrir 2002: 234)。给出一些离散确定性系统的例子将会很有用,这些系统在某种程度上规避了 Gandy 的结论,即每个这样的系统的行为都可以通过图灵机计算。

首先,相对而言,机制满足 Gandy 的四个原则可能会在嵌入了图灵不可计算性的物理定律的宇宙中,例如通过时间变量(Copeland&Shagrir 2007),从可计算输入产生不可计算的输出,这显得相对不重要。此外,一些异步算法不在 Gandy 原则的范围之内(Gurevich 2012;Copeland&Shagrir 2007)。其次,某些(概念上的)离散确定性“相对论计算机”也不在 Gandy 原则的范围之内。相对论计算机是在 Pitowsky 的 1987 年讲座中描述的(Pitowsky 1990),并在 Hogarth 1994 和 Etesi&Németi 2002 中有所提及。这个想法在 物理系统中的计算 条目中有概述;更多讨论请参见 Shagrir 和 Pitowsky 2003,Copeland 和 Shagrir 2020。

Németi 相对论计算机利用引力时间膨胀效应来计算(广义上)一个可以被普适图灵机(例如,停机函数)证明无法计算的函数。Németi 及其同事强调 Németi 计算机“与当前被接受的科学原理并不矛盾”,特别是“量子力学原理并未被违反”。他们进一步建议,人类“甚至可能在未来某个时候”建造一个相对论计算机(Andréka,Németi 和 Németi 2009: 501)。

根据 Gandy 的说法,

"一个离散确定性机械装置满足原则 I-IV"(他称之为“命题 P”;Gandy 1980: 126),和

  1. “What can be calculated by a device satisfying principles I-IV is computable” (he labelled this “Theorem”). 2. “通过满足原则 I-IV 的设备可以计算的内容是可计算的”(他将其标记为“定理”)。

1 and 2 together yield: 邱奇-图灵论题离散确定性机械设备可以计算的内容是可计算的

然而,Németi 计算机是一种离散的、确定性的机械装置,但却能够计算图灵机无法计算的函数。也就是说,相对论计算机是反例,违背了甘迪的 P 论题。简言之,这是因为甘迪原则中隐含的“确定性”概念(“甘迪确定性”)比直观意义上的“确定性”更狭窄,其中确定性系统是指遵循不涉及随机性或随机性的法则的系统。相对论计算机是确定性的,但不是甘迪确定性的。(有关更详细的讨论,请参见 Copeland,Shagrir 和 Sprevak 2018。)

总之,Gandy 的分析对当前对机器计算的理解做出了相当大的贡献。但是,尽管 Gandy 的论点重要且启发人,但它确实没有解决德沃夫论题是否正确的问题。

6.4.3 量子效应和“总体”论题

有一种更强的形式的 Deutsch-Wolfram thesis,在 Copeland 和 Shagrir 2019 年被称为“Total thesis”。

总论题

任何物理系统行为的每个物理方面都可以通过一台通用图灵机计算(以任何指定精度)。

逻辑上,邱奇-图灵论题被通用图灵机本身作为反例(假设通用机器及其无限长的纸带至少是一个概念上的物理系统;有关此假设的讨论,请参阅 Copeland&Shagrir 2020)。这是因为没有算法可以计算通用图灵机是否在每个给定输入上停机 - 也就是说,没有算法可以计算机器行为的这一方面。然而,问题仍然存在,即总论题是否被任何比通用机器“更物理”的系统所侵犯。(请注意,如果存在这样的系统,则不一定也侵犯德沃夫论题,因为有可能,即使关于系统的某些物理问题的答案是不可计算的,该系统仍然可以被图灵机模拟。)

有趣的是,最近在凝聚态量子物理学领域的研究表明,也许量子多体系统可能会违反邱奇-图灵论题。2012 年,Eisert,Müller 和 Gogolin 得出了令人惊讶的结果。

那种确定在重复的量子测量中是否可能出现某些结果序列的非常自然的物理问题是不可判定的,即使对于经典测量而言,同样的问题是容易判定的。(Eisert, Müller & Gogolin 2012: 260501.1)

这是 Cubitt 及其团队 (Cubitt, Perez-Garcia, & Wolf 2015; Bausch, Cubitt, Lucia, & Perez-Garcia 2020; Bausch, Cubitt, & Watson 2021) 关于量子相变不可计算性的一系列戏剧性结果的序幕。这些结果涉及“谱隙”,这是物质性质的重要决定因素。如果系统在系统的基态能级之上有一个明确定义的次低能级,则称量子多体系统为“有隙”,否则称为“无隙”(即能谱是连续的)。“谱隙问题”是确定给定多体系统是有隙还是无隙的问题。

Cubitt 等人的不可计算性结果源于他们发现停机问题可以被编码为谱间隙问题。决定所研究的这类模型系统是有间隙还是无间隙,鉴于局部相互作用的描述,“至少和解决停机问题一样困难”(Bausch,Cubitt 和 Watson 2021: 2)。此外,这不仅仅是“输入不可计算,输出不可计算”的情况。即使初始条件是可计算的(就像 Pour-El 和 Richards 1981 中描述的概念系统一样,见 Section 6.4.1 提到的)。Cubitt 等人强调:

相位图在参数 ϕ 的可计算(甚至是代数)值处甚至是不可计算的。事实上,在 ϕ 的可计算(或代数)值的可数无限集上是不可计算的。 (Bausch, Cubitt, & Watson 2019: 8)

然而,Cubitt 承认证明中使用的模型有些人为

无论结果是否可以推广到更自然的模型,尚有待确定。(Cubitt, Perez-Garcia & Wolf 2015: 211)

简而言之,关于是否存在现实物理系统不能满足邱奇-图灵论题这一问题是一个开放且迷人的问题。

7. 图灵和邱奇的一些关键言论

7.1 图灵机

图灵在他对图灵机的第一次描述之前加了这样一句话:

我们可以将一个正在计算一个...数字的人与一台机器进行比较。(邱奇 1936 [2004: 59])

邱奇-图灵论题是一个模型,在某些方面是理想化的,描述了一个_人类_根据有效方法进行计算的过程。

维特根斯坦以一种引人注目的方式表达了这一观点:

邱奇的“机器”。这些机器是_人类_在进行计算的人。(Wittgenstein 1947 [1980: 1096])

这是邱奇一再强调的要点,以各种形式。例如:

一个配备纸张、铅笔和橡皮,并受严格纪律约束的人,实际上是一台通用机器。 (Turing 1948 [2004: 416])

为了理解图灵的《论可计算数》和后来的文本,必须牢记,当他使用“计算机”、“可计算”和“计算”这些词时,并非指现代意义上的机器,而是指人类计算者。例如:

计算机在写下数字和决定下一步该做什么的时间上总是和实际乘法运算所花费的时间一样长,ACE(自动计算引擎)也是如此……ACE 将会完成大约 10,000 台计算机的工作……计算机仍然会用于小型计算……(邱奇-图灵论题 1947 年[2004:387,391])

图灵的 ACE,一台早期的电子存储程序数字计算机,是在伦敦国家物理实验室建造的;一台试验版本——当时世界上运行速度最快的计算机——首次在 1950 年运行,并且一款商用型号,DEUCE,由英国电气公司非常成功地推出市场。

7.2 人类计算与机器计算

邱奇-图灵论题所描述的通用图灵机蓝图所构建的电子存储程序数字计算机,每一台都在计算上等同于图灵机,因此它们也可以被看作是从事计算的人类模型。图灵选择强调这一点,以一种适合初学者听众的方式来解释这些电子机器:

数字计算机背后的想法可以通过说,这些机器旨在执行任何人类计算员可以完成的操作来解释。(Turing 1950a [2004: 444])

他在包含他对 ACE 设计的技术文件中更准确地阐述了这一观点

那些能够被机器(ACE)解决的问题类别可以被定义得相当具体。它们是那些可以通过人类文书劳动按照固定规则解决的问题的子集,而且是在没有理解的情况下。(Turing 1945 [2005: 386])

图灵继续通过人类职员可用的纸张和时间量来描述这个子集。

这可能是因为他认为这一点对于理解新电子机器的本质是至关重要的,所以他选择在他的《曼彻斯特电子计算机 Mark II 程序员手册》中以这种解释开始

电子计算机旨在执行任何可以由以纪律但无智能方式工作的人类操作员完成的明确经验法则过程。 (邱奇_c_1950: 1)

这不是图灵模拟他的 L.C.M.s 基于_人类_计算机所能实现的想象力不足。他发明图灵机的目的要求如此。_Entscheidungsproblem_是寻找某种_人类可执行_方法的问题,正如前面解释的那样,图灵的目标是要证明在全一阶谓词演算的情况下没有这样的方法。

7.3 邱奇和人类计算机

图灵在他 1936 年的论文中将人类计算机置于中心舞台。而邱奇则没有这样做。邱奇在他关于 Entscheidungsproblem 的两篇开创性论文中都没有明确提到计算或人类计算机 (Church 1936a,b)。他谈到了“有效可计算性”,默认读者会理解这个术语指的是人类的计算。他还使用了“有效方法”这个术语,同样默认读者会理解他在谈论一种可由人类执行的方法。

教会也使用了术语“算法”,说邱奇-图灵论题

很明显,对于任何正整数的递归函数,都存在一种算法,可以有效地计算函数的任何所需特定值。(Church 1936a: 351)

他进一步表示,有效可计算性的概念可以解释如下:

通过定义一个函数为有效可计算的,如果存在一个用于计算其值的算法。(邱奇 1936a: 358)

这是在邱奇对图灵 1936 年论文的评论中,他将人类计算机从阴影中带了出来。他写道:

[A] 人类计算器,配备铅笔和纸张以及明确的指示,可以被视为一种图灵机。因此,很明显,如此定义的可计算性[即,图灵机的可计算性]可以与在某些数学问题中出现的有效性概念等同(特别是,不比)……以及一般涉及算法发现的任何问题。(Church 1937a: 43)

7.4 图灵对“机器”的运用

这一点很重要,当图灵使用“机器”一词时,他通常指的不是一般意义上的机器,而是我们现在所说的图灵机。在某个时候,他明确地指出了这种用法:

“机器处理”这个表达当然指的是那种可以由我在《论可计算数》中考虑的那种机器执行的处理。(Turing 1947 [2004: 378–9])

因此,当图灵在几页之后断言“机器过程和经验法则过程是同义的”(1947 [2004: 383])时,应理解为他正在提出邱奇-图灵论题(及其逆否命题),而不是最大性论题的一个版本。除非记住他的预期用法,否则可能会产生误解。尤其容易误导的是像下面这样的陈述,一个随意读者可能会误以为是最大性论题的一个表述:

邱奇-图灵论题的重要性是明显的。我们不需要有无数不同的机器来完成不同的工作。一个机器就足够了。为不同工作生产各种机器的工程问题被“编程”通用机器来完成这些工作的办公室工作所取代。 (Turing 1948 [2004: 414])

在这个背景下,很明显这些言论涉及与图灵机等价的机器;这段话是嵌入在对 LCM 的讨论中的。

无论图灵是否会在被询问时同意弱极大性论题,目前尚不得而知。毫无疑问,没有任何文本证据支持他同意这一观点。同样适用于 德国-沃尔夫勒姆论题 及其同类:没有任何文本证据表明图灵会同意任何这类论题。

7.5 邱奇的图灵论题版本

有趣的是,邱奇在 1937 年的评论中对图灵关于可计算性的总结并不完全正确。邱奇说:

作者【图灵】提出一个标准,即一个由数字 0 和 1 组成的无限序列被认为是“可计算的”,即应该可以设计一台占用有限空间且工作部件尺寸有限的计算机,如果允许其运行足够长的时间,它将写下序列的任意数量项。(邱奇 1937a:42)

然而,在图灵 1936 年的论文中,并没有提出图灵机需要“占据有限空间”或具有“有限大小的工作部件”的要求。图灵也没有用机器写下“任意数量的项”序列的方式来表述问题,“如果允许运行足够长的时间”。相反,图灵说,一个序列“可计算的条件是它可以被一个无环机器计算”(Turing 1936 [2004: 61]);其中,如果一个机器是无环的,那么它_不_是一个

从不写下超过有限数量的符号[0 和 1]。 (邱奇-图灵论题 1936 [2004: 60])

因此,邱奇对图灵论题的版本与图灵自己的略有不同

邱奇-图灵论题

一个数字的无限序列如果(且仅如果)可以设计一台占用有限空间、工作部件尺寸有限的计算机,让其运行足够长的时间后,就能写下该序列的任意项数,那么这个序列就是“可计算的”。

在邱奇包括这三个有限性要求的范围内(即,机器占据有限空间,具有有限大小的部件,并产生有限数量的数字),他对图灵论题的版本或许可以说比图灵对该论题的任何表述都更“物理”。邱奇的有限性要求在某些方面让人想起甘迪的想法,即离散确定性计算机的状态必须从有限数量类型的基本组件迭代构建,这些组件的维度具有下限(参见 第 6.4.2 节)。尽管如上所述,甘迪对离散确定性计算机施加了进一步的要求,这些要求远远超出了邱奇的有限性要求。

尽管邱奇试图将更多物理现实主义引入图灵机的概念中,但就像图灵的情况一样,不清楚如果询问,邱奇是否会同意 德意志-沃尔夫勒姆论题 或任何类似的论题。没有任何文本证据支持任何一种观点。邱奇对这类问题保持沉默。

补充文件:The Rise and Fall of the​*Entscheidungsproblem*)。

Bibliography

  • Ackermann, Wilhelm, 1928, “Zum Hilbertschen Aufbau der reellen Zahlen”, Mathematische Annalen, 99(1): 118–133. doi:10.1007/BF01459088

  • Aharonov, Dorit and Umesh V. Vazirani, 2013, “Is Quantum Mechanics Falsifiable? A Computational Perspective on the Foundations of Quantum Mechanics”, in Copeland, Posy, and Shagrir 2013: 329–349 (ch. 11).

  • Andréka, Hajnal, István Németi, and Péter Németi, 2009, “General Relativistic Hypercomputing and Foundation of Mathematics”, Natural Computing, 8(3): 499–516. doi:10.1007/s11047-009-9114-3

  • Baldwin, J. Mark, 1902, “Logical Machine”, in J. Mark Baldwin (ed.), Dictionary of Philosophy and Psychology, volume 2, New York: Macmillan, 28–30.

  • Barendregt, Henk, 1997, “The Impact of the Lambda Calculus in Logic and Computer Science”, Bulletin of Symbolic Logic, 3(2): 181–215. doi:10.2307/421013

  • Barrett, Lindsay and Matthew Connell, 2005, “Jevons and the Logic ‘Piano’”, The Rutherford Journal, 1: article 3. [Barrett & Connell 2005 available online]

  • Barwise, Jon, 1977, “An Introduction to First-Order Logic”, in Jon Barwise (ed.), Handbook of Mathematical Logic, Amsterdam: North-Holland, 5–46.

  • Bausch, Johannes, Toby S. Cubitt, Angelo Lucia, and David Perez-Garcia, 2020, “Undecidability of the Spectral Gap in One Dimension”, Physical Review X, 10(3): 031038. doi:10.1103/PhysRevX.10.031038

  • Bausch, Johannes, Toby S. Cubitt, and James D. Watson, 2019, “Uncomputability of Phase Diagrams”, arXiv:1910.01631.

  • –––, 2021, “Uncomputability of Phase Diagrams”, Nature Communications, 12(1): article 452. doi:10.1038/s41467-020-20504-6

  • Behmann, Heinrich, 1921 [2015], “Entscheidungsproblem und Algebra der Logik”, Lecture, 10 May 1921, to the Göttingen Mathematical Society. In Mancosu and Zach 2015: 177–187, with a partial translation by Richard Zach in the same (2015: 173–177).

  • –––, 1922, “Beiträge zur Algebra der Logik, insbesondere zum Entscheidungsproblem”, Mathematische Annalen, 88(1–2): 168–168. doi:10.1007/BF01448447

  • Bernays, Paul, 1918, “Beiträge zur axiomatischen Behandlung des Logik-Kalküls”, Habilitationsschrift, University of Göttingen. Bernays Papers, ETH Zurich (Hs 973.192).

  • Bernays, Paul and Moses Schönfinkel, 1928, “Zum Entscheidungsproblem der mathematischen Logik”, Mathematische Annalen, 99(1): 342–372. doi:10.1007/BF01459101

  • Bernstein, Ethan and Umesh Vazirani, 1997, “Quantum Complexity Theory”, SIAM Journal on Computing, 26(5): 1411–1473. doi:10.1137/S0097539796300921

  • Blum, Lenore, Felipe Cucker, Michael Shub, and Steve Smale, 1998, Complexity and Real Computation, New York: Springer. doi:10.1007/978-1-4612-0701-6

  • Boolos, George and Richard C. Jeffrey, 1974, Computability and Logic, New York: Cambridge University Press.

  • Buss, Samuel R., Alexander S. Kechris, Anand Pillay, and Richard A. Shore, 2001, “The Prospects for Mathematical Logic in the Twenty-First Century”, Bulletin of Symbolic Logic, 7(2): 169–196. doi:10.2307/2687773

  • Calude, Cristian S. and Karl Svozil, 2008, “Quantum Randomness and Value Indefiniteness”, Advanced Science Letters, 1(2): 165–168. doi:10.1166/asl.2008.016

  • Calude, Cristian S., Michael J. Dinneen, Monica Dumitrescu, and Karl Svozil, 2010, “Experimental Evidence of Quantum Randomness Incomputability”, Physical Review A, 82(2): 022102. doi:10.1103/PhysRevA.82.022102

  • Cantor, Georg, 1874, “Ueber eine Eigenschaft des Inbegriffs aller reellen algebraischen Zahlen”, Journal für die reine und angewandte Mathematik, 77: 258–262. doi:10.1515/crll.1874.77.258

  • Carnap, Rudolf, 1935, “Ein Gültigkeitskriterium für die Sätze der klassischen Mathematik”, Monatshefte für Mathematik und Physik, 42: 163–190. doi:10.1007/BF01733289

  • Cassirer, Ernst, 1929, Philosophie der symbolischen Formen (Volume 3: Phänomenologie der Erkenntnis), Berlin: Bruno Cassirer.

  • Church, Alonzo, 1932, “A Set of Postulates for the Foundation of Logic”, Annals of Mathematics, second series 33(2): 346–366. doi:10.2307/1968337

  • –––, 1933, “A Set of Postulates For the Foundation of Logic (2)”, Annals of Mathematics, second series 34(4): 839–864. doi:10.2307/1968702

  • –––, 1935a, “An Unsolvable Problem of Elementary Number Theory, Preliminary Report” (abstract), Bulletin of the American Mathematical Society, 41(6): 332–333. Full paper in Church 1936b.

  • –––, 1935b, letter to Kleene, 29 November 1935. Excerpt in Davis 1982: 9.

  • –––, 1935c, “A Proof of Freedom from Contradiction”, Proceedings of the National Academy of Sciences, 21(5): 275–281. doi:10.1073/pnas.21.5.275

  • –––, 1936a, “An Unsolvable Problem of Elementary Number Theory”, American Journal of Mathematics, 58(2): 345–363. doi:10.2307/2371045

  • –––, 1936b, “A Note on the Entscheidungsproblem”, The Journal of Symbolic Logic, 1(1): 40–41. doi:10.2307/2269326

  • –––, 1937a, Review of Turing 1936, The Journal of Symbolic Logic, 2(1): 42–43. doi:10.1017/S002248120003958X

  • –––, 1937b, Review of Post 1936, The Journal of Symbolic Logic, 2(1): 43. doi:10.1017/S0022481200039591

  • –––, 1941, The Calculi of Lambda-Conversion, Princeton, NJ: Princeton University Press.

  • Church, Alonzo and J. Barkley Rosser, 1936, “Some Properties of Conversion”, Transactions of the American Mathematical Society, 39(3): 472–482. doi:10.1090/S0002-9947-1936-1501858-0

  • Copeland, B. Jack, 1998a, “Even Turing Machines Can Compute Uncomputable Functions”, in Unconventional Models of Computation, Proceedings of the 1st International Conference, New Zealand, Christian S. Calude, John Casti, and Michael J. Dinneen (eds), London: Springer-Verlag, 150–164.

  • –––, 1998b, “Super Turing-Machines”, Complexity, 4(1): 30–32. doi:10.1002/(SICI)1099-0526(199809/10)4:1<30::AID-CPLX9>3.0.CO;2-8

  • –––, 2000, “Narrow versus Wide Mechanism: Including a Re-Examination of Turing’s Views on the Mind-Machine Issue”, The Journal of Philosophy, 97(1): 5–32. doi:10.2307/2678472

  • –––, 2002a, “Accelerating Turing Machines”, Minds and Machines, 12(2): 281–300. (In a special issue on the Church-Turing thesis, edited by Carol Cleland.) doi:10.1023/A:1015607401307

  • ––– (ed.), 2004, The Essential Turing: Seminal Writings in Computing, Logic, Philosophy, Artificial Intelligence, and Artificial Life, Oxford: Clarendon Press. doi:10.1093/oso/9780198250791.001.0001

  • Copeland, B. Jack and Zhao Fan, 2022, “Did Turing Stand on Gödel’s Shoulders?”, The Mathematical Intelligencer, 44: 308–319. doi:10.1007/s00283-022-10177-y

  • –––, 2023, “Turing and von Neumann: From Logic to the Computer”, Philosophies, 8(2): 1–30.

  • Copeland, B. Jack, Carl J. Posy, and Oron Shagrir (eds), 2013, Computability: Turing, Gödel, Church, and Beyond, Cambridge, MA: The MIT Press.

  • Copeland, B. Jack and Oron Shagrir, 2007, “Physical Computation: How General Are Gandy’s Principles for Mechanisms?”, Minds and Machines, 17(2): 217–231. doi:10.1007/s11023-007-9058-2

  • –––, 2011, “Do Accelerating Turing Machines Compute the Uncomputable?”, Minds and Machines, 21(2): 221–239. doi:10.1007/s11023-011-9238-y

  • –––, 2013, “Turing versus Gödel on Computability and the Mind”, in Copeland, Posy, and Shagrir 2013: 1–33 (ch. 1).

  • –––, 2019, “The Church-Turing Thesis: Logical Limit or Breachable Barrier?”, Communications of the ACM, 62(1): 66–74. doi:10.1145/3198448

  • –––, 2020, “Physical Computability Theories”, in Quantum, Probability, Logic: The Work and Influence of Itamar Pitowsky, Meir Hemmo and Orly Shenker (eds), Cham: Springer: 217–231.

  • Copeland, B. Jack, Oron Shagrir, and Mark Sprevak, 2018, “Zuse’s Thesis, Gandy’s Thesis, and Penrose’s Thesis”, in Physical Perspectives on Computation, Computational Perspectives on Physics, Michael E. Cuffaro and Samuel C. Fletcher (eds), Cambridge: Cambridge University Press, 39–59. doi:10.1017/9781316759745.003

  • Copeland, B. Jack and Richard Sylvan, 1999, “Beyond the Universal Turing Machine”, Australasian Journal of Philosophy, 77(1): 46–66. doi:10.1080/00048409912348801

  • Couturat, Louis (ed.), 1903, Opuscules et Fragments Inédits de Leibniz, Paris: Alcan. Facsimile of the 1903 edition, Hildesheim: G. Olms, 1961.

  • Cubitt, Toby S., David Perez-Garcia, and Michael M. Wolf, 2015, “Undecidability of the Spectral Gap”, Nature, 528(7581): 207–211. doi:10.1038/nature16059

  • Curry, Haskell B., 1929, “An Analysis of Logical Substitution”, American Journal of Mathematics, 51(3): 363–384. doi:10.2307/2370728

  • –––, 1930a, “Grundlagen der kombinatorischen Logik, Teil 1”, American Journal of Mathematics, 52(3): 509–536. doi:10.2307/2370619

  • –––, 1930b, “Grundlagen der kombinatorischen Logik, Teil 2”, American Journal of Mathematics, 52(4): 789–834. doi:10.2307/2370716

  • –––, 1932, “Some Additions to the Theory of Combinators”, American Journal of Mathematics, 54(3): 551–558. doi:10.2307/2370900

  • Curry, Haskell B. and Robert Feys, 1958, Combinatory Logic, Amsterdam: North-Holland.

  • da Costa, Newton C. A. and Francisco A. Doria, 1991, “Classical Physics and Penrose’s Thesis”, Foundations of Physics Letters, 4(4): 363–373. doi:10.1007/BF00665895

  • –––, 1994, “Undecidable Hopf Bifurcation with Undecidable Fixed Point”, International Journal of Theoretical Physics, 33(9): 1885–1903. doi:10.1007/BF00671031

  • Davies, E. Brian, 2001, “Building Infinite Machines”, The British Journal for the Philosophy of Science, 52(4): 671–682. doi:10.1093/bjps/52.4.671

  • Davis, Martin, 1958, Computability and Unsolvability, New York: McGraw-Hill.

  • ––– (ed.), 1965, The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions, Hewlett, NY: Raven Press.

  • –––, 1982, “Why Gödel Didn’t Have Church’s Thesis”, Information and Control, 54(1–2): 3–24. doi:10.1016/S0019-9958(82)91226-8

  • Davis, Martin and Wilfried Sieg, 2015, “Conceptual Confluence in 1936: Post and Turing”, in Turing’s Revolution, Giovanni Sommaruga and Thomas Strahm (eds), Cham: Birkhäuser, 3–27. doi:10.1007/978-3-319-22156-4_1

  • Dawson, John W., 2006, “Gödel and the Origins of Computer Science”, in Logical Approaches to Computational Barriers, Arnold Beckmann, Ulrich Berger, Benedikt Löwe, and John V. Tucker (eds), (Lecture Notes in Computer Science 3988), Berlin/Heidelberg: Springer, 133–136. doi:10.1007/11780342_14

  • Dedekind, Richard, 1888, Was Sind und was Sollen die Zahlen? Braunschweig: Vieweg.

  • Dershowitz, Nachum and Yuri Gurevich, 2008, “A Natural Axiomatization of Computability and Proof of Church’s Thesis”, Bulletin of Symbolic Logic, 14(3): 299–350. doi:10.2178/bsl/1231081370

  • Deutsch, David, 1985, “Quantum Theory, the Church–Turing Principle and the Universal Quantum Computer”, Proceedings of the Royal Society of London. Series A. Mathematical and Physical Sciences, 400(1818): 97–117. doi:10.1098/rspa.1985.0070

  • Doyle, Jon, 1982, “What is Church’s Thesis? An Outline”, Laboratory for Computer Science, MIT.

  • –––, 2002, “What Is Church’s Thesis? An Outline”, Minds and Machines, 12(4): 519–520. doi:10.1023/A:1021126521437

  • Earman, John, 1986, A Primer on Determinism, Dordrecht: Reidel.

  • Eisert, Jens, Markus P. Müller, and Christian Gogolin, 2012, “Quantum Measurement Occurrence Is Undecidable”, Physical Review Letters, 108(26): 260501 (5 pages). doi:10.1103/PhysRevLett.108.260501

  • Engeler, Erwin, 1983 [1993], Metamathematik der Elementarmathematik, Berlin: Springer. Translated as Foundations of Mathematics: Questions of Analysis, Geometry & Algorithmics, Charles B. Thomas (trans.), Berlin/New York: Springer-Verlag.

  • Etesi, Gábor and István Németi, 2002, “Non-Turing Computations via Malament-Hogarth Space-Times”, International Journal of Theoretical Physics, 41(2): 341–370. doi:10.1023/A:1014019225365

  • Frankena, William and Arthur W. Burks, 1964, “Cooper Harold Langford 1895–1964”, Proceedings and Addresses of the American Philosophical Association, 38: 99–101.

  • Gandy, Robin, 1980, “Church’s Thesis and Principles for Mechanisms”, in The Kleene Symposium, Jon Barwise, H. Jerome Keisler, and Kenneth Kunen (eds), Amsterdam: North-Holland, 123–148. doi:10.1016/S0049-237X(08)71257-6

  • –––, 1988, “The Confluence of Ideas in 1936”, in The Universal Turing Machine: A Half-Century Survey, Rolf Herken (ed.), New York: Oxford University Press, 51–102.

  • Geroch, Robert and James B. Hartle, 1986, “Computability and Physical Theories”, Foundations of Physics, 16(6): 533–550. doi:10.1007/BF01886519

  • Gödel, Kurt, 1930, “Die Vollständigkeit der Axiome des logischen Funktionenkalküls”, Monatshefte für Mathematik und Physik, 37: 349–360. doi:10.1007/BF01696781

  • –––, 1931, “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I”, Monatshefte für Mathematik und Physik, 38: 173–198. doi:10.1007/BF01700692

  • –––, 1933, “Zum Entscheidungsproblem des logischen Funktionenkalküls”, Monatshefte für Mathematik und Physik, 40: 433–443. doi:10.1007/BF01708881

  • –––, 1934 [1965], “On Undecidable Propositions of Formal Mathematical Systems”, Lecture notes taken by Stephen Kleene and J. Barkley Rosser at the Institute for Advanced Study, in Davis 1965: 39–74.

  • –––, 1936, “Über die Länge von Beweisen”, Ergebnisse eirtes mathematischen Kolloquiums, 7: 23–24.

  • –––, 193?, “Undecidable Diophantine Propositions”, in Gödel 1995: 164–175.

  • –––, 1946, “Remarks Before the Princeton Bicentennial Conference”, in Gödel 1990: 150–153.

  • –––, 1951, “Some Basic Theorems on the Foundations of Mathematics and Their Implications”, in Gödel 1995: 304–323.

  • –––, 1965a, “Postscriptum” to Gödel 1934, in Davis 1965: 71–73.

  • –––, 1965b, letter to Davis, 15 February 1965. Excerpt in Davis 1982: 8.

  • –––, Kurt Gödel: Collected Works, 5 volumes, Solomon Feferman et al. (eds), Oxford: Clarendon Press.

    • 1986, Volume 1: Publications 1929–1936

    • 1990, Volume 2: Publications 1938–1974

    • 1995, Volume 3: Unpublished Essays and Lectures

  • Gurevich, Yuri, 2012, “What Is an Algorithm?”, in SOFSEM 2012: Theory and Practice of Computer Science, Mária Bieliková, Gerhard Friedrich, Georg Gottlob, Stefan Katzenbeisser, and György Turán (eds), (Lecture Notes in Computer Science 7147), Berlin/Heidelberg: Springer, 31–42. doi:10.1007/978-3-642-27660-6_3

  • Guttenplan, Samuel D. (ed.), 1994, A Companion to the Philosophy of Mind, Oxford/Cambridge, MA: Blackwell Reference. doi:10.1002/9781405164597.

  • Hardy, G. H., 1929, “Mathematical Proof”, Mind, 38(149): 1–25. doi:10.1093/mind/XXXVIII.149.1

  • Harel, David, 1992, Algorithmics: The Spirit of Computing, second edition, Reading, MA: Addison-Wesley.

  • Herbrand, Jacques, 1930a, Recherches sur la Théorie de la Démonstration, doctoral thesis, University of Paris. In Herbrand 1968.

  • –––, 1930b, “Les bases de la logique Hilbertienne”, Revue de Métaphysique et de Morale, 37(2): 243–255.

  • –––, 1931a, “Sur le Problème Fondamental de la Logique Mathématique”, Sprawozdania z Posiedzeń Towarzystwa Naukowego Warszawskiego, Wydział III, 24: 12–56.

  • –––, 1931b, Precis of Herbrand 1930a, Annales de l’Université de Paris, 6: 186–189. In Herbrand 1968.

  • –––, 1932, “Sur la non-contradiction de l’Arithmétique”, Journal für die reine und angewandte Mathematik, 166: 1–8. doi:10.1515/crll.1932.166.1

  • –––, 1968, Écrits Logiques, Paris: Presses Universitaires de France.

  • Hermes, Hans, 1969, “Ideen von Leibniz zur Grundlagenforschung: Die Ars inveniendi und die Ars iudicandi”, in Systemprinzip und Vielheit der Wissenschaften, Udo W. Bargenda and Jürgen Blühdorn (eds), Wiesbaden: Franz Steiner: 78–88.

  • Hilbert, David, 1899, Grundlagen der Geometrie, Leipzig: Teubner.

  • –––, 1900 [1902], “Mathematische Probleme”, Nachrichten von der Gesellschaft der Wissenschaften zu Göttingen, Mathematisch-Physikalische Klasse, 3: 253–297. Translated in 1902 as “Mathematical Problems”, Mary Winston Newson (trans.), Bulletin of the American Mathematical Society, 8(10): 437–480. doi:10.1090/S0002-9904-1902-00923-3

  • –––, 1917, “Axiomatisches Denken”, Mathematische Annalen, 78(1–4): 405–415. doi:10.1007/BF01457115

  • –––, 1922, “Neubegründung der Mathematik. Erste Mitteilung”, Abhandlungen aus dem Mathematischen Seminar der Universität Hamburg, 1: 157–177. doi:10.1007/BF02940589

  • –––, 1926 [1967], “Über das Unendliche”, Mathematische Annalen, 95(1): 161–190. Translated as “On the Infinite” in van Heijenoort 1967: 367–392. doi:10.1007/BF01206605

  • –––, 1930a, “Probleme der Grundlegung der Mathematik”, Mathematische Annalen, 102(1): 1–9. doi:10.1007/BF01782335

  • –––, 1930b, “Naturerkennen und Logik”, Die Naturwissenschaften, 18(47–49): 959–963. doi:10.1007/BF01492194

  • Hilbert, David and Wilhelm Ackermann, 1928, Grundzüge der Theoretischen Logik, Berlin: Springer.

  • –––, 1938, Grundzüge der Theoretischen Logik, Berlin: Springer. Second edition.

  • Hilbert, David and Paul Bernays, 1934, Grundlagen der Mathematik, Volume 1, Berlin: Springer.

  • –––, 1939, Grundlagen der Mathematik, Volume 2, Berlin: Springer.

  • Hobbes, Thomas, 1655 [1839], De Corpore, in Thomæ Hobbes Malmesburiensis: Opera Philosophica (Volume 1), William Molesworth (ed.), London: J. Bohn, 1839.

  • Hogarth, Mark, 1994, “Non-Turing Computers and Non-Turing Computability”, PSA: Proceedings of the Biennial Meeting of the Philosophy of Science Association, 1994(1): 126–138. doi:10.1086/psaprocbienmeetp.1994.1.193018

  • –––, 2004, “Deciding Arithmetic Using SAD Computers”, The British Journal for the Philosophy of Science, 55(4): 681–691. doi:10.1093/bjps/55.4.681

  • Hopcroft, John E. and Jeffrey D. Ullman, 1979, Introduction to Automata Theory, Languages, and Computation, Reading, MA: Addison-Wesley.

  • Houser, Nathan, Don D. Roberts, and James Van Evra (eds), 1997, Studies in the Logic of Charles Sanders Peirce, Bloomington, IN: Indiana University Press.

  • Jevons, W. Stanley, 1870, “On the Mechanical Performance of Logical Inference”, Philosophical Transactions of the Royal Society of London, 160: 497–518. doi:10.1098/rstl.1870.0022

  • –––, 1880, letter to Venn, 18 August 1880, Venn Collection, Gonville and Caius College, Cambridge, C 45/4 (quoted by permission of the Master and Fellows of Gonville and Caius).

  • Kalmár, László, 1959, “An Argument Against the Plausibility of Church’s Thesis”, in Constructivity in Mathematics: Proceedings of the colloquium held at Amsterdam 1957, Arend Heyting (ed.), Amsterdam: North-Holland: 72–80.

  • Kennedy, Juliette, 2013, “On Formalism Freeness: Implementing Gödel’s 1946 Princeton Bicentennial Lecture”, Bulletin of Symbolic Logic, 19(3): 351–393. doi:10.1017/S1079898600010684

  • Ketner, Kenneth L. and Arthur F. Stewart, 1984, “The Early History of Computer Design: Charles Sanders Peirce and Marquand’s Logical Machines”, The Princeton University Library Chronicle, 45(3): 187–224. doi:10.2307/26402393

  • Kieu, Tien D., 2004, “Hypercomputation with Quantum Adiabatic Processes”, Theoretical Computer Science, 317(1–3): 93–104. doi:10.1016/j.tcs.2003.12.006

  • Kleene, Stephen C., 1934, “Proof by Cases in Formal Logic”, Annals of Mathematics, second series 35(3): 529–544. doi:10.2307/1968749

  • –––, 1935a, “A Theory of Positive Integers in Formal Logic. Part I”, American Journal of Mathematics, 57(1): 153–173. doi:10.2307/2372027

  • –––, 1935b, “A Theory of Positive Integers in Formal Logic. Part II”, American Journal of Mathematics, 57(2): 219–244. doi:10.2307/2371199

  • –––, 1936a, “General Recursive Functions of Natural Numbers”, Mathematische Annalen, 112(1): 727–742. doi:10.1007/BF01565439

  • –––, 1936b, “λ-Definability and Recursiveness”, Duke Mathematical Journal, 2(2): 340–353. doi:10.1215/S0012-7094-36-00227-2

  • –––, 1952, Introduction to Metamathematics, Amsterdam: North-Holland.

  • –––, 1967, Mathematical Logic, New York: Wiley.

  • –––, 1981, “Origins of Recursive Function Theory”, IEEE Annals of the History of Computing, 3(1): 52–67. doi:10.1109/MAHC.1981.10004

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

  • –––, 1987, “Reflections on Church’s Thesis”, Notre Dame Journal of Formal Logic, 28(4): 490–498. doi:10.1305/ndjfl/1093637645

  • Kleene, Stephen C. and J. Barkley Rosser, 1935, “The Inconsistency of Certain Formal Logics”, Annals of Mathematics, second series 36(3): 630–636. doi:10.2307/1968646

  • Kreisel, Georg, 1965, “Mathematical Logic”, in Lectures on Modern Mathematics, Volume 3, Thomas L. Saaty (ed.), New York: Wiley, 95–195.

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

  • –––, 1974, “A Notion of Mechanistic Theory”, Synthese, 29(1–4): 11–26. doi:10.1007/BF00484949

  • –––, 1982, Review of Pour-El and Richards 1979 and 1981, The Journal of Symbolic Logic, 47(4): 900–902. doi:10.2307/2273108

  • Kripke, Saul A., 2013, “The Church-Turing ‘Thesis’ as a Special Corollary of Gödel’s Completeness Theorem”, in Copeland, Posy, and Shagrir 2013: 77–104 (ch. 4).

  • Langford, C. Harold, 1926a, “Some Theorems on Deducibility”, Annals of Mathematics, second series 28(1/4): 16–40. doi:10.2307/1968352

  • –––, 1926b, “Analytic Completeness of Sets of Postulates”, Proceedings of the London Mathematical Society, second series 25: 115–142. doi:10.1112/plms/s2-25.1.115

  • –––, 1927, “Theorems on Deducibility (Second Paper)”, Annals of Mathematics, second series 28(1/4): 459–471. doi:10.2307/1968390

  • Langton, Christopher G., 1989, “Artificial Life”, in Artificial Life: The Proceedings of An Interdisciplinary Workshop on the Synthesis and Simulation of Living Systems, Held September, 1987 in Los Alamos, New Mexico, Christopher G. Langton (ed.), Redwood City, CA: Addison-Wesley, 1–47.

  • Leibniz, Gottfried Wilhelm, 1666 [2020], Dissertatio de Arte Combinatoria, Leipzig. Translated in Leibniz: Dissertation on Combinatorial Art, Massimo Mugnai, Han van Ruler, and Martin Wilson (eds), Oxford: Oxford University Press, 2020.

  • –––, 1671 [1926], letter to Herzog, October(?) 1671, in Erich Hochstetter, Willy Kabitz and Paul Ritter (eds), Gottfried Wilhelm Leibniz: Sämtliche Schriften und Briefe, second series: Philosophischer Briefwechsel (Volume 1), 1663–1685, Darmstadt: O. Reichl, 1926: 159–165 (facsimile of the 1926 edition, Hildesheim: G. Olms, 1972).

  • –––, 1679 [1903], “Consilium de Encyclopaedia Nova Conscribenda Methodo Inventoria”, in Couturat 1903: 30–41.

  • –––, 1685 [1951], “L’Art d’Inventer”, in Couturat 1903. Translated as “The Art of Discovery” in Philip P. Wiener (ed.),Leibniz Selections, New York: Scribner, 1951: 50–58.

  • –––, 1710, “Brevis descriptio machinae arithmeticae, cum figura”, in Miscellanea Berolinensia ad incrementum scientiarum, pp. 317–19 (and Fig. 73), Berlin: Johann Christoph Papenius.

  • –––, 1714 [1969], letter to Remond, 10 January 1714, in Leroy E. Loemker (ed.), Gottfried Wilhelm Leibniz: Philosophical Papers and Letters, second edition, Dordrecht: Reidel, 1969: 654–655.

  • –––, *n.d.*1 [1903], “De Machina Combinatoria”, in Couturat 1903: 572.

  • –––, *n.d.*2 [1890], “Discours touchant la methode de la certitude et l’art d’inventer pour finir les disputes et pour faire en peu de temps des grands progrés”, in Carl J. Gerhardt (ed.), Die philosophischen Schriften von Gottfried Wilhelm Leibniz (Volume 7), Berlin, 1890: 174–183 (facsimile of the 1890 edition, Hildesheim: G. Olms, 1965).

  • Lewis, Harry R. and Christos H. Papadimitriou, 1981, Elements of the Theory of Computation, Englewood Cliffs, NJ: Prentice-Hall.

  • Llull, Ramon, 1645 [1970], Ars Generalis Ultima, Palma Malorca, facsimile of the 1645 edition, Frankfurt: Minerva, 1970.

  • –––, 1986, Poesies, Josep Romeu i Figueras (ed.), Barcelona: Enciclopèdia Catalana.

  • Löwenheim, Leopold, 1915, “Über Möglichkeiten im Relativkalkül”, Mathematische Annalen, 76(4): 447–470. doi:10.1007/BF01458217

  • MacLennan, Bruce J., 2003, “Transcending Turing Computability”, Minds and Machines, 13(1): 3–22. doi:10.1023/A:1021397712328

  • Mancosu, Paolo and Richard Zach, 2015, “Heinrich Behmann’s 1921 Lecture on the Decision Problem and the Algebra of Logic”, Bulletin of Symbolic Logic, 21(2): 164–187. doi:10.1017/bsl.2015.10

  • Markov, Andrey A., 1951, “Теория Алгорифмов”, Trudy Matematicheskogo Instituta imeni V. A. Steklova, 38: 176–189. Translation by Edwin Hewitt, 1960, “The Theory of Algorithms”, American Mathematical Society Translations, Series 2, 15: 1–14.

  • Marquand, Allan, 1881, “On Logical Diagrams for n Terms”, The London, Edinburgh, and Dublin Philosophical Magazine and Journal of Science, fifth series, 12(75): 266–270. doi:10.1080/14786448108627104

  • –––, 1883, “A Machine for Producing Syllogistic Variations”, in Studies in Logic, Charles S. Peirce (ed.), Boston: Little, Brown, 12–15. doi:10.1037/12811-002

  • –––, 1885, “A New Logical Machine”, Proceedings of the American Academy of Arts and Sciences, 21: 303–307.

  • Massey, Gerald J., 1966, “An Extension of Venn Diagrams”, Notre Dame Journal of Formal Logic, 7(3): 239–250. doi:10.1305/ndjfl/1093958619

  • Mays, Wolfe and Desmond P. Henry, 1951, “Logical Machines: New Light on W. Stanley Jevons”, Manchester Guardian, no. 32677 (14 July 1951) B, 4.

  • –––, 1953, “Jevons and Logic”, Mind, 62(248): 484–505. doi:10.1093/mind/LXII.248.484

  • Mays, W. and Dietrich G. Prinz, 1950, “A Relay Machine for the Demonstration of Symbolic Logic”, Nature, 165(4188): 197–198. doi:10.1038/165197a0

  • Mendelson, Elliott, 1963, “On Some Recent Criticism of Church’s Thesis.”, Notre Dame Journal of Formal Logic, 4(3): 201–205. doi:10.1305/ndjfl/1093957577

  • –––, 1964, Introduction to Mathematical Logic, Princeton, NJ: Van Nostrand.

  • –––, 1990, “Second Thoughts about Church’s Thesis and Mathematical Proofs”, The Journal of Philosophy, 87(5): 225–233. doi:10.2307/2026831

  • Montague, Richard, 1960, “Towards a General Theory of Computability”, Synthese, 12(4): 429–438. doi:10.1007/BF00485427

  • Németi, István and Gyula Dávid, 2006, “Relativistic Computers and the Turing Barrier”, Applied Mathematics and Computation, 178(1): 118–142. doi:10.1016/j.amc.2005.09.075

  • Newell, Allen, 1980, “Physical Symbol Systems”, Cognitive Science, 4(2): 135–183. doi:10.1207/s15516709cog0402_2

  • Newman, Maxwell H.A., 1923, “The Foundations of Mathematics from the Standpoint of Physics”, fellowship dissertation, in the Records of St John’s College, Cambridge, SJCR/SJAC/2/1/5/1 (quoted by permission of the Master and Fellows of St John’s).

  • –––, 1955, “Alan Mathison Turing, 1912–1954”, Biographical Memoirs of Fellows of the Royal Society, 1(November): 253–263. doi:10.1098/rsbm.1955.0019

  • –––, _c_1977, Newman in interview with Christopher Evans, n.d., “The Pioneers of Computing: An Oral History of Computing”, London: Science Museum; transcription by Copeland in Copeland 2004: 206.

  • Olszewski, Adam, Jan Woleński, and Robert Janusz (eds), 2006, Church’s Thesis after 70 Years, Frankfurt/New Brunswick, NJ: Ontos. doi:10.1515/9783110325461

  • Peirce, Charles S., 1886, letter to Marquand, 30 December 1886, in Peirce 1993: item 58, pp. 422–424.

  • –––, 1887, “Logical Machines”, The American Journal of Psychology, 1(1): 165–170.

  • –––, 1903a, “The 1903 Lowell Institute Lectures I–V”, in Peirce 2021: 137–310.

  • –––, 1903b, R S32, draft of last part of the 2nd Lowell Lecture, in Peirce 2021.

  • –––, 1903c, R 462, 2nd draft of the 3rd Lowell Lecture, in Peirce 2021.

  • –––, 1903d, R 464, 3rd draft of the 3rd Lowell Lecture, in Peirce 2021.

  • –––, n.d., R 831, untitled, Charles S. Peirce Papers, Houghton Library, Harvard.

  • –––, 1908, “Some Amazing Mazes (conclusion)”, Monist, 18(3): 416–464. doi:10.5840/monist190818326

  • –––, 1993, Writings of Charles S. Peirce: A Chronological Edition, Volume 5: 1884–1886, Christian J.W. Kloesel (ed.), Bloomington, IN: Indiana University Press.

  • –––, 2021, Charles S. Peirce: Logic of the Future, Writings on the Existential Graphs, Volume 2/2: The 1903 Lowell Lectures, Ahti-Veikko Pietarinen (ed.), Berlin: de Gruyter.

  • Penrose, Roger, 1994, Shadows of the Mind: A Search for the Missing Science of Consciousness, Oxford/New York: Oxford University Press.

  • –––, 2011, “Gödel, the Mind, and the Laws of Physics”, in Kurt Gödel and the Foundations of Mathematics, Matthias Baaz, Christos H. Papadimitriou, Hilary W. Putnam, Dana S. Scott, and Charles L. Harper, Jr (eds), Cambridge: Cambridge University Press, 339–358. doi:10.1017/CBO9780511974236.019

  • –––, 2016, “On Attempting to Model the Mathematical Mind”, in The Once and Future Turing: Computing the World, S. Barry Cooper and Andrew Hodges (eds), Cambridge: Cambridge University Press, 361–378. doi:10.1017/CBO9780511863196.022

  • Péter, Rózsa, 1935, “Über den Zusammenhang der verschiedenen Begriffe der rekursiven Funktion”, Mathematische Annalen, 110(1): 612–632. doi:10.1007/BF01448046

  • Pitowski, Itamar, 1990, “The Physical Church Thesis and Physical Computational Complexity”, Iyyun, 39: 81–99.

  • Post, Emil L., 1936, “Finite Combinatory Processes—Formulation 1”, The Journal of Symbolic Logic, 1(3): 103–105. doi:10.2307/2269031

  • –––, 1943, “Formal Reductions of the General Combinatorial Decision Problem”, American Journal of Mathematics, 65(2): 197–215. doi:10.2307/2371809

  • –––, 1946, “A Variant of a Recursively Unsolvable Problem”, Bulletin of the American Mathematical Society, 52(4): 264–268. doi:10.1090/S0002-9904-1946-08555-9

  • –––, 1965, “Absolutely Unsolvable Problems and Relatively Undecidable Propositions—Account of an Anticipation”, in Davis 1965: 340–433.

  • Pour-El, Marian Boykan and Ian Richards, 1979, “A Computable Ordinary Differential Equation Which Possesses No Computable Solution”, Annals of Mathematical Logic, 17(1–2): 61–90. doi:10.1016/0003-4843(79)90021-4

  • –––, 1981, “The Wave Equation with Computable Initial Data Such That Its Unique Solution Is Not Computable”, Advances in Mathematics, 39(3): 215–239. doi:10.1016/0001-8708(81)90001-3

  • –––, 1989, Computability in Analysis and Physics, Berlin: Springer. [Pour-El and Richards 1989 available online]

  • Quine, Willard Van Orman, 1950, Methods of Logic, New York: Holt.

  • –––, 1951, Mathematical Logic, revised edition, Cambridge, MA: Harvard University Press.

  • Rabin, Michael O. and Dana S. Scott, 1959, “Finite Automata and Their Decision Problems”, IBM Journal of Research and Development, 3(2): 114–125. doi:10.1147/rd.32.0114

  • Ramsey, Frank P., 1930, “On a Problem of Formal Logic”, Proceedings of the London Mathematical Society, second series 30(1): 264–286. doi:10.1112/plms/s2-30.1.264

  • Roberts, Don D., 1973, The Existential Graphs of Charles S. Peirce, Hague: Mouton.

  • –––, 1997, “A Decision Method for Existential Graphs”, in Houser, Roberts, & Van Evra 1997: 387–401.

  • Rosser, J. Barkley, 1935a, “A Mathematical Logic Without Variables. I”, Annals of Mathematics, second series 36(1): 127–150. doi:10.2307/1968669

  • –––, 1935b, “A Mathematical Logic without Variables. II”, Duke Mathematical Journal, 1(3): 328–355. doi:10.1215/S0012-7094-35-00123-5

  • Scarpellini, Bruno, 1963, “Zwei Unentscheidbare Probleme Der Analysis”, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 9(18–20): 265–289. doi:10.1002/malq.19630091802

  • –––, 2003, “Comments on ‘Two Undecidable Problems of Analysis’”, Minds and Machines, 13(1): 79–85. doi:10.1023/A:1021364916624

  • Schiemer, Georg, Richard Zach, and Erich Reck, 2017, “Carnap’s Early Metatheory: Scope and Limits”, Synthese, 194(1): 33–65. doi:10.1007/s11229-015-0877-z

  • Schmidhuber, Jürgen, 2012, “Turing in Context”, Science, 336(6089): 1638–1639. doi:10.1126/science.336.6089.1638-c

  • Schönfinkel, Moses, 192?, “Zum Entscheidungsproblem der mathematischen Logik”, n.d., Heft I, Bernays Papers, ETH Zurich (Hs 974.282).

  • –––, 1924, “Über die Bausteine der mathematischen Logik”, Mathematische Annalen, 92(3–4): 305–316. doi:10.1007/BF01448013

  • Searle, John R., 1992, The Rediscovery of the Mind, Cambridge, MA: MIT Press.

  • Shagrir, Oron, 2002, “Effective Computation by Humans and Machines”, Minds and Machines, 12(2): 221–240. doi:10.1023/A:1015694932257

  • –––, 2006, “Gödel on Turing on Computability”, in Olszewski, Wolenski, and Janusz 2006: 393–419. doi:10.1515/9783110325461.393

  • Shagrir, Oron and Itamar Pitowsky, 2003, “Physical Hypercomputation and the Church–Turing Thesis”, Minds and Machines, 13(1): 87–101. doi:10.1023/A:1021365222692

  • Shepherdson, John C. and Howard E. Sturgis, 1963, “Computability of Recursive Functions”, Journal of the ACM, 10(2): 217–255. doi:10.1145/321160.321170

  • Shoenfield, Joseph R., 1993, Recursion Theory, Berlin/New York: Springer.

  • Sieg, Wilfried, 1994, “Mechanical Procedures and Mathematical Experience”, in Mathematics and Mind, Alexander George (ed.), Oxford: Oxford University Press: 71–117.

  • –––, 2002, “Calculations by Man and Machine: Conceptual Analysis”, in Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman, Wilfried Sieg, Richard Sommer, and Carolyn Talcott (eds), Urbana, IL: Association for Symbolic Logic, 390–409.

  • –––, 2008, “Church Without Dogma: Axioms for Computability”, in New Computational Paradigms, S. Barry Cooper, Benedikt Löwe, and Andrea Sorbi (eds), New York, NY: Springer New York, 139–152. doi:10.1007/978-0-387-68546-5_7

  • Siegelmann, Hava T., 2003, “Neural and Super-Turing Computing”, Minds and Machines, 13(1): 103–114. doi:10.1023/A:1021376718708

  • Siegelmann, Hava T. and Eduardo D. Sontag, 1992, “On the Computational Power of Neural Nets”, in Proceedings of the Fifth Annual Workshop on Computational Learning Theory - COLT ’92, Pittsburgh, PA: ACM Press, 440–449. doi:10.1145/130385.130432

  • –––, 1994, “Analog Computation via Neural Networks”, Theoretical Computer Science, 131(2): 331–360. doi:10.1016/0304-3975(94)90178-3

  • Skolem, Thoralf, 1923, “Begründung der elementaren Arithmetik”, Videnskapsselskapets Skrifter, I. Matematisk-naturvidenskabelig Klasse, 6: 3–38.

  • Smithies, Frank, 1934, “Foundations of Mathematics. Mr. Newman”, lecture notes, St John’s College Library, Cambridge, GB 275 Smithies/H/H57.

  • Stannett, Mike, 1990, “X-Machines and the Halting Problem: Building a Super-Turing Machine”, Formal Aspects of Computing, 2(1): 331–341. doi:10.1007/BF01888233

  • Stewart, Ian, 1991, “Deciding the Undecidable”, Nature, 352(6337): 664–665. doi:10.1038/352664a0

  • Stjernfelt, Frederik, 2022, Sheets, Diagrams, and Realism in Peirce, Berlin: De Gruyter. doi:10.1515/9783110793628

  • Syropoulos, Apostolos, 2008, Hypercomputation: Computing beyond the Church-Turing Barrier, New York: Springer. doi:10.1007/978-0-387-49970-3

  • Turing, Alan M., 1936 [2004], “On Computable Numbers, with an Application to the Entscheidungsproblem”, Proceedings of the London Mathematical Society, 1936, second series, 42(1): 230–265. Reprinted in Copeland 2004: 58–90 (ch. 1). doi:10.1112/plms/s2-42.1.230

  • –––, 1937, “Computability and λ-Definability”, The Journal of Symbolic Logic, 2(4): 153–163. doi:10.2307/2268280

  • –––, 1939 [2004], “Systems of Logic Based on Ordinals”, Proceedings of the London Mathematical Society, second series, 45(1): 161–228. Reprinted in Copeland 2004: 146–204 (ch. 3). doi:10.1112/plms/s2-45.1.161

  • –––, c.1940 [2004], letter to Newman, n.d., in Copeland 2004: 214–216 (ch. 4).

  • –––, 1945 [2005], “Proposed Electronic Calculator”, National Physical Laboratory Report, in Copeland 2005: 369–454 (ch. 20). doi:10.1093/acprof:oso/9780198565932.003.0021

  • –––, 1947 [2004], “Lecture on the Automatic Computing Engine”, London Mathematical Society, in Copeland 2004: 378–394 (ch. 9).

  • –––, 1948 [2004], “Intelligent Machinery”, National Physical Laboratory Report, in Copeland 2004: 410–432 (ch. 10).

  • –––, 1950a [2004], “Computing Machinery and Intelligence”, Mind, 59(236): 433–460. Reprinted in Copeland 2004: 441–464 (ch. 11). doi:10.1093/mind/LIX.236.433

  • –––, 1950b, “The Word Problem in Semi-Groups With Cancellation”, Annals of Mathematics, second series 52(2): 491–505. doi:10.2307/1969481

  • –––, c.1950, Programmers’ Handbook for Manchester Electronic Computer Mark II, Computing Machine Laboratory, University of Manchester. [Turing c.1950 available online]

  • –––, 1954 [2004], “Solvable and Unsolvable Problems”, Science News (Penguin Books), 31: 7–23. Reprinted in Copeland 2004: 582–595 (ch. 17).

  • van Heijenoort, Jean, 1967, From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931, Cambridge, MA: Harvard University Press.

  • Venn, John, 1880, “On the Diagrammatic and Mechanical Representation of Propositions and Reasonings”, The London, Edinburgh, and Dublin Philosophical Magazine and Journal of Science, fifth series, 10(59): 1–18. doi:10.1080/14786448008626877

  • von Neumann, John, 1927, “Zur Hilbertschen Beweistheorie”, Mathematische Zeitschrift, 26(1): 1–46. doi:10.1007/BF01475439

  • –––, 1931, “Die formalistische Grundlegung der Mathematik”, Erkenntnis, 2(1): 116–121. doi:10.1007/BF02028144

  • Wang, Hao, 1974, From Mathematics to Philosophy, New York: Humanities Press.

  • –––, 1996, A Logical Journey: From Gödel to Philosophy, Cambridge, MA: MIT Press.

  • Weyl, Hermann, 1927 [1949], “Philosophie der Mathematik und Naturwissenschaft”, Handbuch der Philosophie, Munich: Oldenbourg. Published in English as Philosophy of Mathematics and Natural Science, Princeton, NJ: Princeton University Press, 1949.

  • Wittgenstein, Ludwig, 1947 [1980], Bemerkungen über die Philosophie der Psychologie. Translated as Remarks on the Philosophy of Psychology, Volume 1, Anscombe, G. Elizabeth M. and Georg Henrik von Wright (eds), Oxford: Blackwell, 1980.

  • Wolfram, Stephen, 1985, “Undecidability and Intractability in Theoretical Physics”, Physical Review Letters, 54(8): 735–738. doi:10.1103/PhysRevLett.54.735

  • –––, 2021, Combinators: A Centennial View, Champaign, IL: Wolfram Media.

  • Yao, Andrew C.-C., 2003, “Classical Physics and the Church-Turing Thesis”, Journal of the ACM, 50(1): 100–105. doi:10.1145/602382.602411

  • Zach, Richard, 1999, “Completeness Before Post: Bernays, Hilbert, and the Development of Propositional Logic”, Bulletin of Symbolic Logic, 5(3): 331–366. doi:10.2307/421184

  • –––, 2003, “The Practice of Finitism: Epsilon Calculus and Consistency Proofs in Hilbert’s Program”, Synthese, 137(1/2): 211–259. doi:10.1023/A:1026247421383

  • Zanichelli, Nicola (ed.), 1929, Atti del Congresso Internazionale dei Matematici, Bologna, 3–10 Settembre 1928, Volume 1: Rendiconto del Congresso Conferenze, Bologna: Società Tipografica.

Academic Tools

Other Internet Resources

Church, Alonzo | computability and complexity | computation: in physical systems | computer science, philosophy of | computing: modern history of | Gödel, Kurt: incompleteness theorems | Llull, Ramon | mind: computational theory of | Turing, Alan | Turing machines

Copyright © 2023 by B. Jack Copeland <jack.copeland@canterbury.ac.nz>

最后更新于

Logo

道长哲学研讨会 2024