数学哲学中的形式主义 formalism (Alan Weir)
首次发表于 2011 年 1 月 12 日星期三；实质修订于 2024 年 2 月 20 日星期二。
形式主义在数学哲学中的一个常见理解是认为数学不是代表现实抽象部分的命题体系，而更类似于一种游戏，与其没有更多的对于对象或属性的本体论承诺，就像玩 ludo 或国际象棋一样。这个想法在直观上是有一定合理性的：考虑那些辛勤学习乘法表或使用标准算法进行函数微分或积分的学生。它也对应于某些时期高级数学家的实践的一些方面，例如在 Bombelli 引入虚数后的一段时间内对虚数的处理，以及一些当代数学家对集合论的高级理论的态度。最后，当被问及数学的本质时，哲学上天真的回答者往往会指向这个立场。因此，鉴于这一观察结果，许多数学哲学家认为“游戏形式主义”是不可行的。本文关注游戏形式主义及其近亲，以及后来的许多发展，其中许多试图克服较粗糙形式的被认知限制。
1. 引言
游戏形式主义的经典之地并非是一个坚定拥护者对该立场的辩护，而是一位伟大的哲学家戈特洛布·弗雷格（Gottlob Frege）对包括 H·E·海因（H. E. Heine）和约翰内斯·托马（Johannes Thomae）在内的真正数学家的工作进行的试图拆除（Frege（1903）《算术的基本法则，第二卷》）。它的相关性部分在于，至少在数学家们思考哲学而非数学的休息日，一些数学家仍然捍卫着类似游戏形式主义的立场。海因和托马是否实际上是游戏形式主义者还存在严肃的问题，我将在下一节中指出。目前必须强调的是，从这个意义上讲，“形式主义”——即弗雷格及其后裔所解释的海因/托马立场——与更复杂的立场（据称）即希尔伯特形式主义是有区别的。有关后者的更多信息，请参阅 Detlefsen（1993）或查阅有关希尔伯特计划和弗雷格-希尔伯特争议的条目。Detlefsen（2005）还对古希腊人到弗雷格和希尔伯特时期以及之后的形式主义主题进行了详细的历史性研究，这也是本文的重点。
虽然在本文中我们将关注非希尔伯特方法，但我们简要讨论一下希尔伯特方法。希尔伯特的立场不同，因为它依赖于数学语言中有限部分和理想部分之间的区别。希尔伯特在哪里划分这个区别，或者应该在哪里划分，是一个有争议的问题。然而，关键是，希尔伯特对理想部分采取了工具主义的态度。这种语言的公式是未解释的，或者被视为未解释的，具有可以应用形式规则进行转换和推理但没有语义的句法形式。尽管如此，如果理想部分在保守地扩展有限部分的基础上，它们是或可以是有用的，也就是说，如果没有从有限前提通过无穷语言绕道到达一个有限结论的证明，我们只使用有限手段就无法得出这个结论，尽管可能需要更长、更不方便的证明（这就是它的实用性所在）。希尔伯特计划的目标是提供一个有限证明来证明这个保守扩展结果；大多数人认为，哥德尔的第二不完备性定理证明了这个目标是不可能实现的。
现在回到我们的非希尔伯特焦点，弗雷格攻击的早期形式主义并没有将数学分为前述的有限/有内容性和无限/本质上无意义的两个对立类别，相反，它以统一和均质的方式对待数学。从现在开始，我将使用“形式主义”来指代非希尔伯特的立场，并将从弗雷格认为在海涅和托马埃身上找到的形式主义观点开始，以及他对它们的批评。现在普遍认为，这些批评包含了对游戏形式主义方法的确凿驳斥。但是有一些后弗雷格观点似乎受到了形式主义的很大影响，或者与之强烈类似。我将依次讨论这些观点：
维特根斯坦关于数学的观点，主要是在他的《逻辑哲学论》中所发现的观念；
逻辑实证主义中的形式主义，特别是卡尔纳普的观点；
古德曼和奎因的名义主义形式主义；
哈斯克尔·柯里的形式主义版本和
柯里-霍华德对应的形式主义解释。
我将以对更近期形式主义哲学家的观察和对当代数学哲学中形式主义前景的总体评估作为结论。
2. 游戏和术语形式主义
弗雷格是一个臭名昭著的对他人解释不友善的人，尤其是随着他年纪的增长。但是最近的学术研究（特别是参见劳伦斯，2023 年）表明，在他对汉克尔、海涅和托马等形式主义对手的解释中，他的理解特别偏离了实际情况。然而，弗雷格的地位如此崇高，以至于他对他们观点的扭曲解释在包括我在内的形式主义哲学家的著作中被广泛接受，包括之前版本的本条目。
或许弗雷格犯的最重要的错误是假设当托马埃谈论数学作为一种用符号玩的游戏时，弗雷格认为符号是具体的标记，即“通过在物体的表面上书写或印刷而产生的图形（黑板、纸张）”（弗雷格 1903/1980，§98）[1]。事实上，托马埃经常使用“符号”来表示表示，例如无限小数被构想为实数的表示：
一个无限小数是...一个缩写，一个对通常的有限小数序列的符号，或者是被分配给这样一个序列的符号（托马埃 1898: 5）[2]
而这些表示是潜在无限的，而不是实际上的无限序列，因此肯定不是无限的，甚至不是不可行的大型具体符号。因此，弗雷格讽刺地评论道：
为了产生它 [一个无限序列]，我们需要一个无限长的黑板，无限的粉笔供应和无限的时间。我们可能会因为试图用这样一个平凡的反对意见来压制如此高尚的精神而受到指责；但这并不是答案。（弗雷格，1903/1980，§124：199）
本身也应受到指责，因为它对无限潜力的理解过于教条主义地予以否定。
汤玛思的思想也受到他对魏尔斯特拉斯分析方法的同情的影响，而不是黎曼分析方法（对于弗雷格来说，情况正好相反）。魏尔斯特拉斯认为，基于幂级数的代数方法可以用于实数和复数分析：
∞∑n=0a0+a1(x−c)+a2(x−c)x2…an(x−c)n…
其中术语 ai 只包含代数运算符，如算术函数加法、乘法和指数运算，这些概念比利曼的概念更严格，利曼的概念使用了“超越”的非代数运算符。在托马埃对这些思想的阐述中，一个关键点是算术运算符操作的对象并不重要，只要它们无论是什么，都遵守“游戏”的代数规则即可。因此，他对形式主义的理解更接近于我们现在所称的结构主义。所以当他说：
现在，对于形式概念来说，算术是一个带有符号的游戏，我们可以称之为空的，从而传达出（在计算游戏中）除了在某些组合规则（游戏规则）下赋予它们的行为属性之外，它们没有其他内容属于它们。（托马埃，1898 年，3 页）。
关键短语是“（在计算游戏中）没有其他内容属于它们”。Thomae 并不否认数字术语具有或可以具有“内容”的意义，即它们可以指称-“命名”-方程的程度，例如（Thomae，1898：3）。但是，在对无限序列的（有限初始段）进行算术运算时，我们“括号”除了属于操作符的内容之外的任何内容，就像我们在检查数学推理的逻辑正确性时，忽略了自然语言半正式扩展中的短语的含义-忽略了“实数”，“函数”等短语的含义，仅仅关注论证中句子的形式结构。
总之，Frege 所攻击的形式主义是一个稻草人立场。但这是一个历史上重要的立场，不仅与 Frege 的解释学有关，而且因为它是后来哲学家以此为出发点构建的一个立场，或者是要避免的一个死胡同。对于 Frege 来说，任何类似形式主义的东西都是一条死胡同，因为他认为算术是一套由表达式表达的真理，其中数值表达式指代独立于思想（或至少独立于任何特定个体思想）的抽象指称。Frege 说 Heine 和 Thomae 谈论数学领域和结构，禁止发表某些特殊意义上的言论（例如，反对写“3÷0”，在某种特殊意义上被认为是无意义的），数字之间的大小关系（而不是物理标记的大小或亮度）-所有这些，Frege 指出，如果算术是一种标记及其物理属性的理论，或者仅仅是一套无指称符号的转换，都是没有意义的。然而，他未能考虑到，他们之所以以这种方式表达自己，是因为他们实际上并没有将算术视为处理无意义具体标记的操作。
从历史上看，弗雷格的反形式主义批评中提炼出了两种不同的教科书观点，Resnik（1980: 54）和 Shapiro（2000: 41–48）将其描述为术语形式主义和游戏形式主义。术语形式主义认为数学表达式（例如算术）是有意义的，单数术语是指涉的，但是指涉的是像它们自己这样的符号，而不是作为与符号不同的实体的数字。然而，游戏形式主义坚持数学话语没有意义；或者至少其中出现的术语不指代对象和属性，这些话语不能用来陈述事实。相反，数学是一个根据固定规则转换“空”符号串的演算法。因此，游戏形式主义对于任何希望阻止、避免或回避（以某种方式）对一个问题领域的抽象对象的本体论承诺的人来说是有吸引力的。因为标准数学涉及了大量的定理，肯定了无限领域的实体的存在——数字、函数、集合、态射、范畴等等，这些实体似乎不是具体的，实际上，似乎很难融入一个彻底自然主义的现实观念中。
游戏形式主义是对反实在论者来说唯一的选择，他们担心订阅抽象对象的本体论。相比之下，术语形式主义将数学解释为关于符号的一种语法理论。然而，标准的语法理论涉及了无限的实体——表达式类型，它们看起来和数字一样抽象。实际上，正如哥德尔对语法的算术化所示，标准形式语法的元素和相互关系可以被建模为算术标准模型内的一个无限子结构。因此，术语形式主义对于反实在论者似乎没有用处。
当然，形式主义的句法和证明理论后来成为数学的一个分支。弗雷格抱怨海涅和托马没有提供一个远远不足以作为他们所处理的数学的解释的句法和证明理论。这是正确的，但是需要像弗雷格这样的人物通过引入前所未有的严谨标准来革新数学的形式化。他认识到（§90：185-6）可以将数学理论、它们的语言、公理和规则作为形式化的数学对象来处理。这正是希尔伯特计划成功实现的目标，创造了新的元数学学科。
鉴于这些工具，一个严谨的形式主义者应该如何按照弗雷格的意义进行？她将通过阐明基本元素——原始符号和它们的字符串——来对形式语言进行描述，并给出哪些字符串符合良构的递归规范。同样地，我们将得到一个严格的规范，说明在给定系统中哪些良构公式的排列被视为证明，以及在每种情况下它们证明的定理是什么。如果像“3+1=0”或“3>2”这样的字符串在系统中被证明是可行的（比如说在模 4 算术中），那么这足以将它们视为系统的正确表述。不需要进一步考虑真实性问题，也不需要假设对于给定的符号集只有一个系统。此外，我们也不需要假设每个系统都是完备的（尽管弗雷格对托马埃的算术演算的不完备性提出了批评，尽管这个问题很容易纠正）。我们不需要假设这些字符串中的数字引用系统之外的任何东西，事实上我们甚至不需要假设它们引用任何东西。因此，这种严格的游戏形式主义不受“3>2”应该被视为假的反对意见的影响，无论如何合法的形式主义解读“>”；也不需要将数字视为指代具体标记，而“>”则意味着在物理上更大。
因此，这样一个形式主义者避免了弗雷格对他所归因于海因和托马的立场提出的一些异议。但是，他提出了两个主要的异议，这些异议仍然适用于使用现代元数学工具发展起来的游戏形式主义。第一个是适用性的问题：如果数学只是一个我们在其中洗牌未解释符号（或其解释无关紧要的符号），那么为什么它在如此多的方面、如此多的不同事物（普通物体、亚原子物体、场、属性，甚至从数学的一部分到另一部分）上都被成功应用了呢（我们可以计算纯几何空间中的维度数量）？弗雷格写道：
现在，正是适用性使得算术从一种游戏升华为一门科学。（弗雷格 1903/1980：167 节）
其次，弗雷格非常正确地坚持区分了“游戏”——算术、集合论、拓扑学或其他任何东西——仅仅作为一个数学对象本身，一个形式系统，以及游戏的理论。“让我们记住，游戏的理论必须与游戏本身区分开来”（§107，183）。因此，在三角学的“游戏”中，我们可以推导出
sin2θ+cos2θ=1
来自毕达哥拉斯定理。在元理论中，我们可以证明：
⊢⟨sin2θ+cos2θ=1⟩,
主张在数学语法的数学表示中具有某种代码的公式（在这里由“⟨sin2θ+cos2θ=1⟩”表示的代码）是可证明的。同样，在元理论中，我们可以证明关于证明和反驳的许多其他事情，例如我们可能能够显示许多句子既不可证明也不可反驳。
这对形式主义者提出的问题如下：元理论本身是一种实质性的数学，表面上致力于无限的对象领域，这些对象本身并不具体。对象语言游戏演算的表达式令牌可能是有限的——墨迹之类的；但由于有无限多的表达式、定理和证明，这些本身必须被视为抽象类型。最多，形式主义者只能从某些数学理论（如集合论）的超穷领域减少承诺，转向可数无穷但仍然是抽象的算术领域，其中标准可数语言（如标准集合论的语法和证明理论）可以像哥德尔所示那样被建模。这对于术语形式主义可能足够了，尽管将所有数学归结为语法理论不会得到数学家们的认可（关于此，请参见下面关于 Curry 的部分）。但如果我们假设他们受到某种反实在论的动机，那对于游戏形式主义者来说是不够的。
形式主义能否以一种方式发展，以克服这两个关键的反对意见，即适用性问题和元理论问题（我将其称为元理论问题）？（虽然这些不是形式主义的唯一反对意见，但它们是两个基本的反对意见。）由于弗雷格的批评并没有扑灭后来的数学哲学家中的所有形式主义冲动，我们现在将看看未来的发展，看看它们的表现如何。
3. 形式主义的《论逻辑哲学》
维特根斯坦是弗雷格作品的热心学生，他在弗雷格亲自访问耶拿期间，由弗雷格本人指导他进一步研究伯特兰德·罗素的工作。因此，人们可能认为他对形式主义有所免疫。但是，在维特根斯坦的《逻辑哲学论》中，确实出现了明显的形式主义元素。
当然，众所周知，《逻辑哲学论》是一部难以解释的作品。甚至对于这本书的主要部分（除了前言和结尾的“框架”之外的所有内容）是否被视为对形而上学的认真尝试的问题都存在争议。如果我们将这种解释争议放在一边，考虑到我们所提供的形而上学，我们发现形式主义的方面有两个。首先，数学句子被称为表达“伪命题”，因此没有真值（只有偶然命题具有真值）。其次，数学被描述为一种“演算法”，不用于表示世界本身，而完全是工具性的。当然，这种最明确的陈述不在《逻辑哲学论》中，而是在维特根斯坦写给拉姆齐的评论中提到的。
数学的基本思想是运算的思想，这里用操作的思想来表示。逻辑的开始预设了计算和数。数是微积分的基本思想，必须作为这样引入（Lewy，1967：421-2）。
在《论逻辑哲学》中，我们确实得到了数学命题只是工具的思想（所有数学，而不仅仅是一个“理想”的片段，如希尔伯特所说）：
实际生活中，数学命题从来不是我们想要的。相反，我们只在从不属于数学的命题到同样不属于数学的其他命题的推理中使用数学命题（在哲学中，“我们实际上用这个词或这个命题做什么？”这个问题反复引导我们获得有价值的洞见）（《论逻辑哲学》第 6.211 段）。
这个思想以以下陈述为前提：
数学是一种逻辑方法。数学的命题是方程，因此是伪命题。（同上，第 6.2 段）
数学的命题并不表达一个思想。（同上，第 6.21 段）
然而，必须小心谨慎。维特根斯坦区分了那些无意义的言辞（包括逻辑重言和矛盾）和那些荒谬的言辞；数学言辞属于哪一类并不清楚。人们可能会认为，形式主义者应该将数学言辞视为荒谬的，而不仅仅是无意义的，因为在这种观点下，它们只是一串毫无意义的符号。然而，与形式主义明显不同的是：对于维特根斯坦来说，数学不应被看作是与语言的其他用途分离的一种演算法。相反，他试图展示至少部分算术可以被看作是基于非数学语言用法的。相比之下，弗雷格则认为，算术（和分析）的适当解释应该展示其普遍性如何使人能够对多种不同的应用给出统一的解释（参见达梅特，1991 年第 20 章），同时也强烈主张数学言辞具有独立于其在应用中使用之前的意义。
Wittgenstein 在《论理哲学》中并未尝试超越算术的数学理论，而且仅限于算术的一个相当狭窄的片段。这一理论明显与形式主义者的反柏拉图主义观点相一致。在这里，没有数字，算术被解释为一种通过操作指数或运算符的指标来进行计算的方法。什么是运算符？Wittgenstein 将运算符术语与函数术语区分开来，但评论家们一直在努力解释这种区别的含义。显然，Wittgenstein 认为应用于不同字符串 t 和 u 的函数术语 f 的两个出现具有不同的含义，其中“含义”是指 Wittgenstein 所指的指称，类似于 Frege 的 Bedeutung。因此，“f”在“f(t)”中所指的实体与“f(f(t)”中最外层的 f 所指的实体不同；这被认为是解决罗素悖论的基础（第 3.333 段）。特别是，“the father of”在“the father of John”中的意义与其在“the father of the father of John”中最外层的出现中的意义是不同的。换句话说，没有真正的函数迭代应用，这对于许多人来说，与疾病一样糟糕的罗素悖论的解决方案。
然而，运算符与函数至少在一个方面有所区别：运算符的真正迭代——命题逻辑的句子运算符是一个典型的例子——可以在不假设一个令牌从一个到另一个的意义或指称的变化的情况下进行。那么它们的意义或指称是什么？维特根斯坦否认它们有任何指称，这是他关于逻辑常量不是代表的主张的概括。彼得·希尔顿（1997 年：96-98）认为，维特根斯坦在《论述》中谈到“函数”时，心中想的是罗素的命题函数，并且竭力区分运算符与这些“实质性”实体。罗素的命题函数与普通数学函数不同，后者是弗雷格函数概念的模型。它们是结构化实体，与作为其值的命题有结构上的关联——可以将其视为不完整的事态。相比之下，运算符不代表任何这样的实体，它们既不是命题的部分，也不是任何种类的命题成分，在命题中“不留痕迹”。
句子运算符被构想为将符号、铭文映射到其他符号和归属，而是将命题（在维特根斯坦对该术语的相对粗糙的理解中）映射到命题。根据维特根斯坦对命题的解释，对否定等操作的重复应用...p,∼p,∼∼p...可能会使人回到一个较早的点。尽管如此，维特根斯坦试图用句子运算符应用于非数学语言来阐明算术。（在此可以看到，柯奇在后来严格推导出类似思想的处理数字的 λ 演算中，将数字视为重复应用输入函数的函数。）用口号形式来说，数字是运算的指数（同上，第 6.021 段）。因此，如果 Ω 是运算符的示意符号，Ωp（或 Ω（p））表示其应用于命题，那么我们可以看到这个系列
p,Ωp,ΩΩp,ΩΩΩp,ΩΩΩΩp,…
作为“数字定义”的起点，通过将其重写为
Ω0p,Ω0+1p,Ω0+1+1p,Ω0+1+1+1p,Ω0+1+1+1+1p,….
在这里，我们有无限多个示意性的重写规则。像“0+1+1+1+1”这样的指数可以用数字来简写，简写方式显而易见，例如“0+1+1+1+1”可以简写为“4”等等。
维特根斯坦的例子表明（尽管他没有明确说明）两个数/指数的相加 Ωnp+Ωmp（同样适用于 Ωn+mp）遵循以下规则：
Ωnp+Ωmp⇒Ωn(Ωmp)
告诉我们可以用公式右边的表达式替换左边的表达式。
这就是“正确性”的基础，例如 n+m=r 这样的等式，除了对维特根斯坦来说，这样的等式并不表达一个真理。根据他的解释，等号在语言的完全分析中消失了，在这种分析中，通过名称的相同和不同来显示相同和不同，其中在完全分析的语言中，没有两个名称引用同一个对象（这种观点为将《论述》中的数学表达解释为无意义提供了依据）。维特根斯坦本人并没有费心去证明放弃等号不会削弱语言的表达能力，但其他人，如 Hintikka（1956）和 Wehmeier（2004）已经这样做了。在去除等号的基础语言中，剩下的是替换规则（《论述》第 6.23 段）。
这些规则必须以一般和概要的方式进行解释。因此，当我们将 ∼ 替换为 Ω 时，我们发现（维特根斯坦在这里没有直觉上的顾虑）双重应用 ∼∼p 会使我们回到（具有相同意义的）p。但这并不能证明 2=0 的真实性，因为对于许多其他操作，ΩΩp 并不等同于 p。另一方面，
ΩΩ(ΩΩΩp) 总是与 ΩΩΩ(ΩΩp) 有相同的意义
维特根斯坦隐含地假设括号与运算符的适当规则，特别是广义结合律。（实际上，他使用括号和符号 Ω′p 的混合表示 Ω(p)。）
由于方程 Ωnp=Ωmp 在其基本逻辑形式上不是一个全称普遍化 ∀n,m(Ωnp=Ωmp)，而是一个纯粹的示意性普遍化，因此没有形式 ∃n,m(Ωnp≠Ωmp) 可以用来表达不等式，即使我们可以理解 '≠' 的含义。我们也不能将不等式 n≠m 示意地表达为对于每个 Ω 的选择，Ωnp 与 Ωmp 的不等价成立。否则，2≠0 将会失败，因为 ∼∼p 等价于 p。《论逻辑哲学》的理论无法处理不等式。
至此，我们已经讨论了加法及其解释在这个运算中的局限性。那么乘法呢？维特根斯坦在第 6.241 段定义了乘法：
Ωn×mp⇒(Ωn)mp
但要理解这个作为一般原则的定义，我们需要知道如何解释符号(Ωn)m。在更传统的数学中，人们可能会简单地将(xn)m 定义为 xn×m，但显然这样做（或者说对于指数运算符的相互作用的等效定义）会在维特根斯坦的解释中引入循环性。或者，我们可以借助指数的递归理论来解释，即 am×0=a，am×(n+1)=am+am×n。由于归纳原理在维特根斯坦的体系中并未出现，这些规则可能被视为原始规则。
总的来说，维特根斯坦在《论述》中对数学的总体解释并不包括除了一部分算术之外的其他内容，基本上只涉及到仅涉及加法的正等式。在那里，他否认这些句子表达了具有真值的命题。当然，这本书是在极其困难的情况下写成的。也许尽管上述困难，他的解释可以进一步发展并更具说服力，但对于这一点的怀疑，可以参考兰迪尼（2007）的观点。当维特根斯坦在 20 世纪 20 年代与 F.P.拉姆齐和维也纳学派合作时，并没有尝试这样做。如果维特根斯坦的立场无法进一步发展，我们可以选择放弃除了加法算术之外的所有数学，或者拒绝《论述》的解释。在这里，我们并不需要盲目地对当代数学持批判态度，就可以看出合理的选择是什么。诚然，拒绝《论述》的解释也是维特根斯坦自己似乎在书的结尾所采取的选择；在这里，我们进入了一个问题，即为了在最后抛弃它，为什么要带我们经历这样一个奇怪而不令人信服的理论。（有关对维特根斯坦《论述》立场更积极的评价，请参见弗洛伊德（2002）的观点。）
维特根斯坦关于数学哲学的后期著作，例如《关于数学基础的注释》（1956/1978 年），长期以来甚至比《论理哲学》的解释更少得到认可，尽管最近哲学家如朱丽叶特·弗洛伊德和希拉里·普特南姆已经为其辩护，认为它是一个有趣且见解独到的数学解释（弗洛伊德/普特南姆，2000 年）。其中的主题包括对实际无限的否定（事实上，他的著作倾向于强有限主义）；否认不可判定的句子具有意义；拒绝康托尔的幂集证明；认为证明的发现改变了所涉及术语的含义；以及其他非常激进的观点。其中我们发现对形式主义主题的持续坚持：
在数学中，一切都是算法，没有意义；（《哲学语法》：468）。
维特根斯坦思想中的另一个持久主题是数学的意义完全存在于其在非数学应用中的实用性。但是，关于这种适用性如何产生的系统理论不存在，例如，没有证明一个保守扩展定理，即数学演算应用于经验前提将永远不会导致我们得出一个不符合这些前提的经验结论。而且，关于元理论的问题也没有解决。另一方面，我们应该注意到，这些维特根斯坦关于数学哲学的笔记并非由他本人出版，而是在他去世后由他人出版的。关于维特根斯坦的整体数学哲学观的概述，请参阅《维特根斯坦的数学哲学》。
4. 形式主义与实证主义者
维特根斯坦对维也纳学派产生了很大的影响。所谓“官方”的实证主义数学理论并不是形式主义的理论。数学定理以一种特殊的方式表达真理：仅凭意义本身而真实。最有影响力的实证主义者是卡尔纳普，如果我们不将奎因归类为实证主义者的话（但奎因的观点在 1930 年代至少非常接近卡尔纳普的观点，事实上可以说奎因对于那个时代的卡尔纳普的激进经验主义更为忠实）。在卡尔纳普的一些著作中，我们当然可以看到强烈的形式主义元素，例如在《语言的逻辑语法》（1934/1937）和《经验主义、语义学和本体论》（1950/1956）中。
前一本书于 1937 年被翻译成英文，名为《语言的逻辑语法》。在这本书中，卡尔纳普认为哲学的正确方法是进行概念分析，即被理解为“逻辑语法”，大致上是指语法本身和证明论。为了解决哲学上的分歧，人们提议将争议的立场规范化为形式语言或“框架”，其中包括一套公理和证明规则；在给定这些规则的情况下，一些句子是“确定的”，可以被证明或证伪。这些是相对于该框架的分析性和矛盾性的句子。我们如何选择采用哪个系统？卡尔纳普的“宽容原则”（1934/1937）允许我们选择任何我们希望的系统：
在逻辑学中，没有道德规范。每个人都有权利按照自己的意愿建立自己的逻辑，即自己的语言形式。[原文中的斜体]
卡尔纳普将这种无拘无束的宽容心态扩展到数学领域，并将其强加给数学家们：
这种宽容的态度，就特定的数学演算而言，是大多数数学家心照不宣的共识。[同上]
任何这样的演算法都可以被视为数学的一部分，即使是不一致的。通过淡化或直接丢弃语义概念，我们只是绕过了关于数学所“关于”的实体性质的传统本体论争议。唯一的问题是任何给定数学演算法的实用性，或者说其他方面。
这里出现了一些问题。卡尔纳普如何区分经验的科学理论和数学理论？其次，如果实用性主要是经验应用的问题，那么卡尔纳普的形式主义者如何知道给定的演算法将如何保守地扩展经验理论，又如何在没有引用有意义的数学结果的情况下知道这一点？卡尔纳普写道：
形式主义观点在于认为系统的构建可以纯粹地形式上实现，也就是说不涉及符号的含义；...但是，这样勾勒出来的任务显然不能仅通过构建逻辑数学演算法来完成。因为这个演算法不包含...那些与数学应用有关的句子...例如，“这个房间里现在有两个人”这个句子不能仅仅通过形式主义者通常构建的逻辑数学演算法来推导出来，而是可以通过逻辑主义系统的帮助来推导，即基于弗雷格对“2”的定义。（卡尔纳普 1934/1937，326）
添加（斜体为卡尔纳普的）“这种结构同时满足形式主义和逻辑主义的要求。”
但是，有什么能阻止我们根据宽容原则自由地规定“桥梁原则”，使其在证明论上的行为类似于数值运算符——“ϕ 的数量”——通过其在算术公理的表述中的定义性出现，并且桥梁原则包括以下内容：
ϕ 的数量=0↔∃x(ϕx&∼∃y(ϕy&y≠x))ϕ 的数量=1↔∼∃xϕx？
也就是说，我们将零的数词与陈述有恰好一个适当类型的实体相连，将一的数词与陈述没有这样的实体相连。如果我们这样做，添加标准十进制算术的规则，然后尝试应用这个演算法，将会发生灾难；但是，我们不需要一个有内容的保守扩展结果来表明对于我们使用的演算法，不会发生灾难吗？
哥德尔的不完全性定理在这方面和其他方面对卡尔纳普提出了非常困难的问题。第一个不完全性定理告诉我们，在任何（ω-）一致的形式理论中，其定理是可递归枚举的，并且包含一定（相当有限）数量的算术的情况下，将存在一个算术句子，既不能被证明，也不能被其否定所证明。在卡尔纳普的术语中，这似乎产生了非确定性的句子，如果我们确信其中一些句子仍然是真实的话，这对他来说是一个问题；而且用于证明不完全性结果的关键类型的句子——“哥德尔句子”——实际上在算术的标准模型中是真实的，如果这些句子以适当的方式构造（有不同的方法可以做到这一点），从一个在该模型中本身是真实的理论中。
哥德尔本人写了一篇批判卡尔纳普立场的论文，但并未发表（哥德尔，1953-9）。哥德尔关注的不是他的第一不完备定理，而是他在第二定理中得出的推论：在对一种特定的一致性属性进行自然描述的情况下，这种描述可以通过他对语法的算术化来进行数学上的表达，哥德尔所考虑的那种形式理论无法证明自身的一致性。他认为，为了证明数学演算法没有经验内容，从而支持他的实证主义论点，卡尔纳普需要为数学演算法提供一致性证明，以表明它们不具有经验内容，事实上，通过涵盖所有经验句子，它们具有丰富的经验内容。然而，沃伦·戈德法布（1995 年：328）指出，这一观点未能认识到卡尔纳普在 1937 年的立场中的深层整体性，其中分析与综合的区别是相对于所讨论的系统、"语言框架" 而言的。（当然，这种深层整体性具有违反直觉的后果，即数学和经验科学之间没有超越框架的区别。）
卡尔纳普实际上理解了哥德尔的定理的重要性（Tennant，2008）；他直接从哥德尔那里了解到了这些结果，哥德尔确实阅读了《逻辑语法》的草稿。尽管如此，他对于这些结果对他的立场的影响显示出了令人瞩目的漠不关心。他承认，在证明一致性时，需要转向一种更强的语言（§60c），并自由地使用了数学技术，这些技术在任何意义上都不能被归类为有限的（例如，在 §14 中，他使用了具有无限前提的规则，特别是后来被称为 ω 规则的规则）。通过这种方式，他至少可以否认对于算术来说存在任何非确定性的句子，因为每个真实的算术句子都可以使用 ω 规则来证明（相对于一个相当弱的有限逻辑，远比经典逻辑和弱公理系统如 Q-罗宾逻辑要弱）。
卡尔纳普的放松态度源于他放弃了对认识论基础的追求。如果一个人希望通过对形式主义解释的诉诸来确保我们对数学的知识，那么寻求希尔伯特所追求的一致性证明是有意义的，人们将寻求从一个有限的片段中对整个数学的证明，相对于这个片段，我们的知识似乎很难受到质疑。但是，卡尔纳普，也许是受到哥德尔的深刻定理的影响，似乎已经放弃了这个目标，并认为宽容原则使他免于任何这样的需求。人们可以规定自己喜欢的任何东西，包括更强的公理系统，从中可以证明较弱理论的一致性。这并不为相信或接受较弱的理论提供任何更坚实的理由，但无论如何也不需要这样的理由。
如今很少有人在数学中寻求笛卡尔式的确定性，所以卡尔纳普在这里的立场似乎是合理的。然而，他是否已经解决了适用性的问题并不那么清楚。即使保守扩展结果只能在一个更强大的系统中给出，如果我们希望对我们即将在设计桥梁或计算机时使用的特定演算法有实用性的保证，我们需要这个结果是一个有内容的真理，而不仅仅是一串我们可以从某个系统中推导出来的符号。如果卡尔纳普主义者承认这个结果是一个有内容的真理，我们可以问，根据这个形式主义立场，构成这个真理的是什么。卡尔纳普确实受到了对卷入形而上学争论的恐惧的驱使。但是，如果他的立场不仅在认识论上没有野心，而且如此泄气，以至于只能说一些关于数学和科学理论形式化的元数学技术可以应用于，那么它也就失去了所有哲学上的兴趣，并且不再对数学哲学的辩论做出干预。
卡尔纳普并非真的放弃了形而上学：这位曾经的形而上学反对者实际上是一个拥有自己对立理论的兄弟形而上学家，正如 F.H.布拉德利可能会说的那样。因此，后来的《经验主义、语义学和本体论》的主要意义在于通过（极具争议的）“内部”问题与“外部”问题之间的区别，将本体论的担忧视为伪问题。其中，“内部”问题由框架的规则来解决，这些框架可以是数学、普通的“事物”谈论或其他什么。而对于这些外部问题，卡尔纳普声称，没有真值命题与之相对应；例如，对于这样一个问题，没有形式为“是的，存在无限多的抽象数”的真实答案。相反，它们应该通过决策来回答，这些决策是基于关于框架相对于所讨论的话语目标的效率、富有成效性和实用性的实用标准来做出的。但是这些目标可能是什么呢？是预测“感知数据”的流动，这些数据被认为是构成世界的最终家具吗？如果是这样，我们可以看到，所吹嘘的本体论中立是虚伪的，我们有了一种激进的经验主义反实在主义形而上学。
形式主义的痕迹在于：卡尔纳普认为“正确性”是由规则来确定的，这些规则统治着一个系统，而不是由与规则系统无关的事实领域的对应来确定。他认为这种方法消解了本体论的担忧，并使我们摆脱了对于我们这样有限的、有血有肉的生物如何能够获得关于这个独立事实领域的详细知识的任何解释义务，这个领域是由卡尔纳普揭示为一个形而上学的幻觉的抽象、非时间性、非因果性对象和属性的配置领域。与形式主义的一个重要不同之处在于，卡尔纳普将这种观点应用于所有领域的话语，而不仅仅是数学。
5. 名义主义形式主义
W. V. Quine 著名地反对实证主义者关于真理在于意义和准逻辑主义数学观念的学说（部分原因是他也反对他的导师 Carnap 的内部/外部区分）。与 Nelson Goodman 合作，他们提出了一种形式主义宣言。他的形式主义阶段似乎没有持续很长时间：后来他采取了一种数学唯物主义形式，淡化了对“名义主义”的相对年轻时期的迷恋，甚至可以说是忽视了。但在这段时间里，他和 Goodman 通过直接解决其他形式主义者回避或忽视的问题，大大推进了形式主义的讨论。
Goodman 和 Quine 的《走向建设性名义主义的步骤》（1947）提出了一种毫不妥协的游戏形式主义：
从使用数学公式中所获得的自然科学的收益并不意味着这些公式是真实的陈述。没有人，甚至是最坚定的实用主义者，会认为算盘上的珠子是真实的；我们的观点是，像算盘上的珠子一样，形而上学数学的公式是方便的计算工具，不需要涉及真理问题。（122）。
他们将数学的句子仅仅视为没有意义的符号串
以此来解释形式主义
以及随附/监督的概念
数学所具有的这种可理解性源于规定那些标记的句法或元数学规则。(111)
值得称赞的是，古德曼和奎因并没有回避元理论问题，即句法和元数学本身似乎与算术一样本体论丰富，并致力于抽象对象。相反，他们正视这个问题，并试图完全依靠有限数量的具体对象的本体论来解决（然而，他们确实假设了相当强大的部分整体原则，特别是普遍组合：他们假设任何一组对象，无论多么分散或分散，也是一个部分整体对象 - 一个“融合”或“总和” - 有良好的地位。）
他们非常巧妙地尝试开发一种句法，将“将数学表达式视为具体对象”（同上）-作为实际的物理标记，并为“公式”，“公理”和“证明”等概念提供具体的替代品，如柏拉图式定义。然而，他们没有解决以这种具体的形式主义方式解释数学应用的问题。
除了适用性问题之外，Goodman 和 Quine 提出的形式主义还存在两个关键问题。首先，他们是否有权利对句法提出一般性的主张，将其解释为关于某些具体标记和标记融合的理论，尚不清楚。因此，在他们通过“准公式”来定义公式并得出我们想要的结果时，他们说：
通过要求“x”中的下一个更复杂的替代否定也是准公式的替代否定，该定义确保这些替代否定在直观上预期的意义上也将成为公式；以此类推，直到“x”本身。（116）
（“替代否定”是 Sheffer 竖线操作“P|Q”，当且仅当其中一个分量为假时，该操作为真。）问题出在“以此类推”上。Goodman 和 Quine 试图通过一个任意的公式逐步推进，以展示他们的定义将确保每个更大的组成部分都是公式。然而，对于任意的“x”，我们如何能够保证这一点，而不需要类似于公式复杂性的归纳之类的东西？但是，由于公式不是按照通常的归纳集合论方式生成的，因此这种保证是不可用的。类似的评论也适用于在第 120 页上以名义主义方式定义的证明，它们在直观上预期的立场上具有前提和结论之间的内部顺序。证明通过对一个具体证明中编号为“k”的公理进行泛化，然后依次对它们进行选择。这似乎预设了关于所有数字的概括的真实性，而且确实需要可数选择，这些资源对于严格的名义主义者来说是不可用的。
其次，Goodman 和 Quine 对于像“222222+1 是质数”这样的句子能说些什么呢？
（也就是说，用“2^n”表示“2 的 n 次方”，“[2^(2^(2^(2^(2^2))))]+1 是质数”；参见 Tennant，1997 年，152 页。）他们不能否认这个句子的存在，因为我们眼前就有这个符号。但是有充分的理由认为，没有任何具体的证明或证伪存在，因为唯一可用的方法可能会消耗比任何人都能拥有的时间、空间和材料更多，甚至可能超过实际存在的数量。有无数个具有这种特性的句子：它们的具体符号存在，但实际上不存在任何具体的证明或证伪，也没有任何一个人可以将其作为有意义的话语来操作。（参见 Boolos，1987 年。）Goodman 和 Quine 的形式主义者似乎被迫得出这样的结论：像上面那样的句子，在通常的形式意义上是可判定的，既不是真的也不是假的，既不具体可证明也不具体可证伪。然而，接受这种观点将会对当前实践的数学进行破坏；这样的结果应该被视为他们立场的荒谬推论。
(That is—with ‘2^n’ representing ‘2 to the power n’—‘[2^(2^(2^(2^(2^2))))]+1 is prime’; cf. Tennant, 1997,152.) They cannot deny the sentence exists, for there is the token before our very eyes. But there are strong grounds for thinking that no concrete proof or disproof will exist, for the only methods available may use up more time, space and material than any human could have at her disposal, perhaps than actually exists. There are countless sentences with this property: concrete tokens of them exist but no concrete proof or refutation actually exists, none that a human could manipulate as a meaningful utterance anyway. (Cf. Boolos, 1987.) Formalists of Goodman and Quine’s persuasion seem forced to the conclusion that sentences like the above, sentences which are decidable in the usual formal sense, are neither true nor false, since neither concretely provable nor concretely refutable. To embrace this view, however, would be to butcher mathematics as currently practised; such a consequence should rather be viewed as a reductio ad absurdum of their position.
6. 形式主义术语：Curry
非希尔伯特形式主义数学哲学中最实质性的尝试是 Haskell Curry 的著作《数学形式主义概要》（Curry, 1951）。Curry 并不是一个游戏形式主义者，他的立场更接近于术语形式主义，这是我们起初提出的两种观点之一。然而，Curry 的数学哲学，至少在他认为自己可以在数学的本体论承诺问题上保持中立的程度上，是一种高度反形而上学的哲学。
数学可以被构想成一门科学，以至于它独立于除了最基本的哲学假设之外的任何其他假设。（3）
因此，他并不是被反柏拉图主义者对抽象对象的恐惧所驱使。事实上，他的中立性在某种程度上受到了妥协，因为柯里完全乐意承认一种无限的本体论，其中包括了可能是抽象表达类型的对象。正式地说，他对于他的形式系统的原语（他误导性地称之为“标记”）并不感兴趣：
对于这些标记，我们可以选择任何我们喜欢的对象，同样地，我们可以选择任何具有所需形式属性的组合这些对象的方式作为运算符。（28）
但由于对于许多系统来说，存在着无限多的原始“标记”，它们并不能都与数学家实际产生的具体标记相对应。
像形式主义一词一样，Curry 认为数学在经过哲学反思后，可以被恰当重建，其本质上具有句法学科，即形式系统。然而，与 Frege 的对手不同，Curry 在形式数学学科发展之后撰写，能够对形式系统给出更严格的（尽管在他的情况下有些古怪）解释。对于形式系统的公理、规则和定理的形式没有任何限制。形式系统中的基本命题的真值仅仅取决于它们在系统中的可证性。他的一个形式系统（示例 7：23）只有一个谓词“由 Gödel 用“ist beweisbar”这个词表达的一元谓词”（23），即可证性谓词。该系统的基本真值可以被解释为关于底层系统中可证性的陈述。任何通常类型的形式系统都可以被“简化”为只有一个可证性谓词的系统，并且在简化系统中，元命题 ϕ 的真值（=可证性）仅在 ϕ 在简化系统中可证时成立：⊢⟨ϕ⟩（34-35）。Curry 允许通过通常的逻辑运算符来从基本命题中构建复合命题，以便用证明论的语言来表达复杂命题（第九章）。
No restrictions are placed on what form the axioms, rules and therefore theorems of a formal system are to be. Truth for elementary propositions of a formal system consists simply in their provability in the system. One of his formal systems (Example 7: 23) has only one predicate “a unary predicate expressed by Gödel by the words ‘ist beweisbar’” (23), i.e., a provability predicate. The elementary truths of this system can be interpreted as claims about provability in the underlying system. Any formal system of the usual sort could be ‘reduced’ into one in which there is only one provability predicate and truth (= provability) in the reducing system of the elementary proposition ϕ holds only when ϕ is provable in the reduced system: ⊢⟨ϕ⟩(34–35). Curry allows that one can form compounds from elementary propositions by means of the usual logical operators in order to express complex propositions in the language of proof theory (Chapter IX).
形式主义的结果是，数学总体上变成了元数学，一种有内容的理论——Curry 的句子表达具有真值的命题——阐述了关于在底层形式系统中从什么中可证明什么的真理，其解释，或者说解释们，并不被认为在数学上很重要。然而，这种立场威胁着崩溃为结构主义，将数学话语视为隐含地概括了一系列（一般而言）满足这些概括的抽象结构。至于元理论的问题，Curry 并不试图回答这个问题；除了通过只考虑标准形式系统，可以使用可数的本体论来扮演语言表达式的角色之外，没有真正的尝试避免对对象的丰富本体论的承诺。然而，这样做的代价是严重扭曲数学实践。集合论者、拓扑学家、分析学家等等提出猜想，并试图证明关于集合、拓扑空间、复数函数等等的事情。在他们哲学的时刻，他们可能会想知道他们所努力解决的概念是关于什么的，但他们一般不会提出猜想或试图证明关于表达式字符串的事情，除非这对他们在证明关于集合、空间、复平面等等的事情时具有工具价值（参见 Resnik：70-71）。
7. Curry-Howard 对应关系
Haskell Curry 在将逻辑与计算机科学联系起来的发展中也发挥了重要作用，一些人认为这可以支持数学中的形式主义。他在组合逻辑方面的工作以及 W.A. Howard 的工作导致了“Curry-Howard 对应关系”（以下简称“CH”）或“CH 同构”，将逻辑、证明理论和计算机科学联系起来。
Curry 打算提供一个功能性的一般理论，作为逻辑的基础，“预逻辑”，正如 Curry 所称。特别是参见（Curry 1934）和与 Robert Feys 合著的（Curry and Feys 1958）。在 Curry 在该领域首次发表论文的同时，Alonzo Church 开发了他的无类型 λ 演算，也旨在为逻辑，甚至更广泛地说是数学，提供基础，并将函数作为基本概念。在这些函数演算中，（有关详细解释请参见 Barendregt（1984），以及关于 λ 演算的条目）使用串联 fg 来表示将函数 f 应用于参数 g，从而产生输出值。参数和值本身也可以是函数，并且允许自我应用。而 Curry 的系统是无变量的，Church 的系统通过 λ 项进行变量绑定，如果变量 x 在 N 中出现，则在 λx.N 中绑定。λ 演算中的基本操作是 β-还原，这个转换将我们从（λx.N）M 转换为 N [x:=M]。这里 N [x:=M] 是将 M 替换为 N 中所有自由出现的 x 的结果。因此，例如，（λx.xx）f β-还原为 ff。我们可以将其写为：
(λx.xx)f⊳ff
因此，这些演算实现了维特根斯坦在《论述》中（见上文）似乎在他的操作/函数区分中所指的，因为在 Church 和 Curry 中，我们有一个完全发展的“操作”理论，即可以将函数作为参数和值的函数。当然，自我应用，如无限循环的 β-还原：
(λx.xx)(λx.xx)⊳(λx.xx)(λx.xx)⊳(λx.xx)(λx.xx)⋮
引发了悖论可能出现的担忧。邱奇认为避免使用自由变量并限制排中律（Church, 1932: 346–7）可以阻止悖论，但是克里尼和罗瑟（1935）使用基于理查德悖论的策略表明，该系统是平凡的：可以使用规则推导出每个公式。邱奇修复了这个问题，以产生一致的无类型 λ 演算，但是与 CH 对应关系相关的重要步骤是发展有类型的 λ 演算。
现在，“类型”是一个非常过度使用的词。那种类型的标记，使用其中一个意义（大致上是抽象的句法对象），有时被用来代表属性，包括高阶属性，如罗素的各种类型理论中。教堂在他的简单类型化的 λ 演算版本中继续了这一传统（教堂，1940 年）。在这种用法中，类型，如犬性或形状性质，有实例，如菲多，在第一种情况下，或在第二种情况下，是低阶属性的正方形。因此，在这个意义上，类型的实例不一定是抽象对象。另一种用法是句法的，当一种语言的基本表达式被划分为各种不相交的类别（“类型”），并且制定了用于生成良好形成表达式的形成规则，利用了类型的区别。在这种用法中，“类型”是语言的句法元理论中的一个表达式。在某些情况下，句法理论实际上是所讨论的对象理论的一部分。独立于此，一些句法类型理论的表述将句法元理论“推下来”到所讨论的对象理论中，通过规定对象语言的良好形成表达式包含句法适当部分，就像标签一样，这些部分与表达式的元理论类型相关联，并且没有语义角色。例如，在霍华德（1969）中，命题逻辑条件片段的良好形成公式被用作类型符号，作为类型理论的上标术语。
通常读作“N:τ”的表达式
术语 N 的类型是 τ
因此，可以以多种方式阅读，例如：
I：非句法：由 N 所指的实体是 τ 所指的类/集合/属性的一个实例，该实例不一定是句法的，更一般地说，也不是抽象的。
II：元句法：由 N 所指的表达式是 τ 的句法范畴的一个实例。将术语归类到类型的句法理论是“元”的，相对于背景智力背景而言，在该背景中，它并不是以（在其预期解释下）作为提供语法的语言中更一般理论的一部分呈现的。
III: 句法学：表达式 N 是句法类别 τ 的一个实例，而类型理论是它所属语言的一个句法理论。
尽管一些类型理论的教科书对于逻辑学家来说似乎有些模糊，不确定上述“类型”的解释是否存在问题，但这通常不适用于这些理论的先驱者。例如，霍华德在他的经典论文《公式即类型的构造概念》中写道：
这个标题有第二个缺陷；即，类型应该被视为一个抽象对象，而公式是类型的名称。（1969 年：479）
并区分类型和类型符号（480）。
虽然后来发展出了各种类型理论的非句法模型，例如（Scott，1970），并且对集合论基数做出了相当强的假设，比如存在不可达基数。对于形式主义者来说，更相关的是“术语模型”，这些是类似于语言解释的句法模型，它们使用自己的符号作为域的成员，在 Henkin 完备性证明中可以找到这些解释；尤其是“句法语义”方法，例如 Per Martin-Löf 直觉主义类型论的某些解释（参见直觉主义类型论条目），或者 Peter Schroeder-Heister 的“证明论语义”（参见证明论语义条目），这些方法避免了通过“外部”真值条件来赋予类型和术语意义的尝试：数学语言不应被视为对某个独立现实的表示。
在这样的背景下，“类型”的元句法和句法解读之间的区别并不是很重要。重要的是类型理论的公理和推理规则使我们能够证明关于类型的元定理。这种情况可以类比于序列演算和自然推理之间的关系，前者的推导关系 ⊢ 可以解释为某个基础自然推理系统中的可导关系，而序列演算提供了关于对象语言可导性的高阶定理。因此，无论一个人是否将类型视为元理论概念，类型理论的演算可以证明关于术语 N 是类型 τ 的定理。
现在，Curry 在 1934 年的工作以及与 Feys 在 1958 年的更全面的合作，展示了条件理论中可证明公式与类型理论中基本组合子类型之间的某种对应关系。特别地，以→作为条件符号，以 α⇒β 表示函数类型，即（非句法解释的）类型，其输入为 α 类型的函数，输出为 β 类型的函数，我们有以下关系（这里 ⊢T→表示在正（非相关主义）条件理论中的可证明性，⊢CL 表示在适当的组合逻辑中的可证明性）：
⊢T→A→B 当且仅当存在某个 N，使得 ⊢CLN:α⇒β
其中 N 是由基本组合子构建的术语，α 在结构上同构于 A（同样 β 同构于 B）。也就是说，通过将命题语言中的公式的句子字母以基本类型的名称进行统一替换（可能是平凡的恒等替换），可以从 A→B 生成 A⇒B，其中每个→的出现都被 ⇒ 替换。
Curry 和 Feys（1958）将对应思想扩展到类型理论和 Gentzen 的序列演算之间。在已经引用的论文中，该论文于 1969 年开始流传，但直到 1980 年在为 Curry 举办的纪念会上的一本专题论文集中才正式发表。W.A. Howard（1969）通过展示直觉主义序列形式自然演算和 λ 演算格式的类型理论之间的对应关系，进一步加深了 CH 对应关系的研究。该研究将直觉主义算术（“Heyting 算术”）纳入其中（因此需要从命题逻辑扩展到谓词逻辑），作为对构造主义概念的研究项目的一部分。Howard 通过明确表示不仅是序列演算中可证明的公式与类型赋值之间的对应关系，而且还包括类型赋值中的术语与相应公式的证明之间的对应关系。[4] 例如，（令相关主义者感到恐惧的是）A →（B → A）在 T→中是可证明的。相应的类型是 α⇒（β⇒α），这是基本运算符 K 的类型，其作用是
NM⊳N
其 λ 表示为（λx.（λy.x））（通常缩写为 λxy.x），这可以通过 β-还原链看出：[5]
(λx.(λy.x)N)M⊳(λy.N)M⊳N.
在 T→ 中，A → (B → A) 的最简单证明是：
A1B→AA→(B→A)1
图 1
其中第二步，到中间结论 B → A，是→I（引入）的一个实例，具有未假定前提 B 的空洞释放（在序列演算版本中，将使用细化规则，在序列前提中添加额外假设）。类型理论证明中的类型理论 TT [6] 构造一个“居住”于类型 α⇒(β⇒α)的术语的形式如下：
xt: x:αxλy.x:β⇒αλxy.x:α⇒(β⇒α)x
图 2
在这里，λ 抽象，即 λ 项的引入，对应于→I，因此 λ 项 λxy.x 的类型为 α⇒(β⇒α)，“编码”了→I 的类型相关的两个步骤，即引入函数类型的规则 ⇒I（第一个应用是一个虚无放电的例子），我们可以恢复上述命题定理的证明。此外，鉴于类型理论计算和某些类型的编程语言中的程序之间的紧密联系，我们还可以将 TT 证明视为构建某种类型的计算对象的步骤的程序。
在自然演绎系统中，规范化是消除冗余推理循环的过程。在某些逻辑（如直觉逻辑）中，存在一个规范化元定理，告诉我们任何证明都可以剥离其冗余部分，并平滑地简化为正常形式。霍华德提出的进一步的对应关系将规范化与程序的“评估”联系起来，在这种程序中，复杂的术语被简化为最简形式（在更具表达能力的类型系统中，这并不总是可能的）。
似乎是 Kreisel 引入了“公式即类型”的口号，而 Martin-Löf 则负责更广泛的“命题即类型”口号（再次参见 Wadler，2015）。在哲学背景下，“命题”常常被用来表示类似于句子的意义，即某种类型的公式的意义。使用这个术语，一种广泛的直觉主义立场是，公式所表达的命题是该公式的所有证明的集合（或种类，对于直觉主义者而言）。鉴于不同的可证公式将对应不同的类型，CH 对应关系使我们能够将这个“句法-语义”立场重新表述为：HA 的公式所表达的命题是其证明的类型，其中“类型”不是“集合”或“种类”的直接同义词，而是来自 λ-演算的概念。正如已经指出的，这个演算是一个与编程和计算机科学有着丰富相互关系的形式系统，其中类型的实例完全是句法的，例如证明论实体。因此，在这样的解读中，公式的意义，即所表达的命题，并不代表与公式所出现的语言系统不同的现实。
与直觉主义的联系是明确的：但 CH 对形式主义的相关性是什么？首先，某些形式主义立场与某些直觉主义之间存在明显的重叠。当然，并不是指创始人布劳尔的哲学直觉主义，其数学对象本体论为心智建构，数学知识的认识论基于对思想连续性的内部反思；这是远离形式主义的数学形而上学。但许多构造主义者在不接受他的形而上学的情况下，接受了布劳尔的数学正确性（如果愿意谈论数学真理，则为真理）与可证明性的等同或紧密联系。这种等同对某种形式主义来说更加合适，这种形式主义拒绝了数学命题代表一种独立于思维的现实，并且还根据那些在某个形式系统中可证明的命题与那些可证伪的命题来区分数学中的优秀与劣质。
但直觉主义者和形式主义者之间也存在实质性的差异。首先，不仅布劳尔，而且许多后来的构造主义者都拒绝将可证明性与某个形式系统中的可证明性等同起来。其次，形式主义者通常自由运用经典逻辑，并强调数学家的自由创造力：她应该自由生成任何她希望的数学理论，只要在选择的背景逻辑中，如果发现不一致，就应该撤回这些理论。
在第一个观点上，形式主义者当然会成为一个形式主义者！她将正确性与形式证明联系起来，至少在最基本的层面上。在这里，CH 对应关系，或者更好的说法是对应关系，对形式主义者肯定非常有吸引力。命题与计算之间的联系，特别是将编码证明的术语的算法化简为不可约的正常形式，非常契合那些将数学视为只是符号洗牌而没有外部参照的形式主义版本。
在第二个观点上，对 CH 对应关系的进一步研究将结果从直觉逻辑推广到各种其他逻辑，特别是经典逻辑（Griffin，1990），以及其他逻辑框架，如模态逻辑和线性逻辑。这样，“公式即类型”并没有施加繁重的逻辑限制，形式主义者没有必要束手束脚地战斗。
形式主义者所珍视的自由创造力如何呢？构造性类型理论当然已经远远超越了 Heyting 算术；尤其雄心勃勃的扩展可以在基于同伦类型理论的单价基础项目中找到（Awodey，2014）。因此，基于“公式即类型”的形式主义可能会追求这条道路。但对于希望在非构造性数学方面保持非修正主义的形式主义者来说，前景可能不太明确。仅仅添加产生特定理论的额外公理或推理规则是不够的，在标准框架中，例如一阶或高阶语言的框架。因为还需要进一步的工作来证明该系统中存在 CH 对应关系的扩展。
此外，在形式主义的证明论属性方面（直觉主义逻辑满足的），素性也存在问题，即当 ⊢ A ∨ B 时，要么 ⊢ A，要么 ⊢ B。经典理论通常没有这个属性，除非是否定完备的，这将对推广 CH 对应关系和证明排中律（假设形式主义者不仅仅将所有非平凡演算视为合法而无需证明）造成问题。如果相对于特定框架，数学主张的正确性与可证性等同，并且在既不可证明的情况下，一个析取式可以是正确的，那么形式主义者似乎需要一些花哨的手法来证明使用经典逻辑的合理性（超值论在这里并不明显适用）。
还有一个适用性的问题，弗雷格认为这对形式主义者来说是一个无法克服的问题。应用数学概念，例如“ϕ 的数量”，在其中混合了数学和非数学的论述，其含义是什么？除非 CH 形式主义者希望走上邓美特的反实在论道路，并将证明的概念推广为适用于经验语言的验证概念，否则她将不得不找到一种方法，将纯数学的证明论语义与不同的、可能是实在主义的、真值条件语义相结合，而不会过于特别为此而设立。
最后需要注意的是，如果我们可以这样称呼它的话，CH 形式主义对于那些受反实在论关注并希望将抽象对象从所有数学中（包括元数学）排除的形式主义者来说是不可接受的。根据 CH 形式主义，数学公式的具体表达的意义是证明的集合/种类/类型，而后者是无限多的、任意长的有限长度的抽象对象。换句话说，元理论的问题尚未解决。反实在论者不能简单地借用句法-语义学的思想，并应用 CH 对应关系来支持反实在论；需要进行更多的哲学工作。
8. 当代形式主义
后来的发展主要集中在形式主义运动的“希尔伯特派”中。P.J.科恩关于广义连续统假设的研究与哥德尔的相对一致性证明一起表明，当前公理无法判定它以及与集合的基数有关的无数相关集合论命题。在没有明显的、非特定的方法来扩展公理以解决这些问题的情况下，一些数学家，如科恩本人（科恩，1971 年）和亚伯拉罕·罗宾逊（Robinson，1965 年；1969 年），对高阶集合论的现实解释感到绝望。因此，他们将那些没有合理的公理集来解决关键问题的数学分支视为数学的“理想”部分，缺乏其他领域所具备的内容。
关于游戏形式主义，尽管哲学家们可能指责数学家倾向于陷入这种看似不受认可的立场，但很少有哲学家提出类似于游戏形式主义者的观点。Gabbay（2010）和 Azzouni（2004；2005；2006；2009）都站在形式主义旗帜下。Gabbay 的形式主义（他仅在引用的论文中对算术进行了发展）占据了“传统形式主义、虚构主义、逻辑主义和现实主义之间的丰富中间地带”（Gabbay，2010：219）。此外，他写道：“与传统（游戏）形式主义相反，我的提议不涉及试图为每个算术真理提供形式推导”（Gabbay，2010：221）。
Azzouni 将他的“形式主义版本”（Azzouni，2004：105）描述为普通数学证明“指示”形式推导。指示关系相当开放：Azzouni 并不声称所指示的推导都属于一个单一的形式系统；相反，普通证明可以指示来自“一系列”形式推导的推导。然而，Azzouni 说，所指示的推导不一定存在；当然，它们的具体标记也不一定存在于指示它们的非正式证明的同一时期。古希腊几何学中的证明指示了 21 世纪或之后的推导。实际上，它们可能永远不存在-它们可能太长而无法写下（Azzouni，2006：154），尽管这些不存在的证明被认为可以解释数学家对哪些非正式证明是正确的的共识！在后来的工作中，Azzouni 似乎对这种（或任何）形式主义退却了：
我（不情愿地）一直陷入这样一种观点，即数学家在阅读非正式的数学证明时必须参与类似于复杂的句法模式识别的活动，以便他们对不存在的形式推导背景敏感（而不自知）。 （Azzouni，2009：25）
转向对数学推理的“推理包”视角，这种视角似乎并不形式主义：再次参见 Azzouni（2009）。
然而，还有一群当代数学哲学家的观点似乎接近形式主义，即（其中的一些）虚构主义者。现在，“虚构主义者”这个术语可能会误导，因为并非所有虚构主义者都将数学与虚构相同等。即使有人这样做了，问题也会出现：“对虚构和关于虚构的话语，我们采取什么样的哲学解释？”许多哲学家都不赞成将虚构人物视为现实本体论，就像许多人拒绝将数学视为现实主义（柏拉图主义）的本体论一样。对于虚构主义的非常简单的反现实主义可能会将诸如“奥利弗·特威斯特在伦敦出生”这样的陈述分析为真实（或正确），只要该句子或其同义词在狄更斯的小说中出现（Field，1989：3）。即使这对于虚构作品有效，显然对于数学来说是荒谬的。如果一个数学命题在一本期刊中被宣布为定理，无论是否有证明，即使这个主张从未受到质疑并且被数学界接受，这并不意味着该命题是真实的（或正确的，如果不喜欢将真理谓词应用于数学句子）。考虑到有多少“定理”的所谓证明后来被发现是不正确的，我们可以相当确定一些谬误将错误地被接受为永远被证明的。此外，将有无数的数学命题，有些是真实的，有些是错误的，从未出现在数学文献中，从未被实际的数学家考虑过。
现在，奥利弗·特威斯特的例子归功于虚构主义学派的创始人 Hartry Field，如果我们可以这样称呼他的话。但他对自己的立场作了以下限定：
我们大多数人认为奥利弗·特威斯特只是在小说中说过或者由此导致奥利弗·特威斯特住在伦敦（1989 年，3）[我强调]。
不管这对于小说是否有效（如果作品不一致怎么办：必须使用相关的因果关系吗？如何处理类似托尔斯泰/陀思妥耶夫斯基的不同作品之间的比较？），这是一个具有明显形式主义色彩的有趣的数学立场。数学家可以提出任何（一致的）理论。然后，该理论的真理只是该理论的结果，无需认为该理论代表了外部现实。玛丽·伦格（2010 年）对这种虚构主义进行了研究。但一个关键问题是：如何理解“结果”？对于形式主义者来说，这必须是推导性的结果。但伦格拒绝这样的解读：她的虚构主义是一种在逻辑结果不是从句法上解释而是从模态上解释的虚构主义，其中所涉及的必然性是原始的。因此，这种虚构主义的子类不能被归类为形式主义。
相比之下，韦尔明确地接受形式主义（1991 年；1993 年；2010 年；2016 年），而且是游戏形式主义传统中的形式主义。他的立场，如果与虚构主义相比，可以被看作是在形式主义传统中以句法的方式解读“结果”，即以形式推导的方式解释。作为第一个近似，该立场认为，如果存在一个具体的推导令牌，数学句子就是真的；如果存在一个具体的推导令牌，它的否定就是假的。由于真实性和虚假性条件不涉及抽象证明，这种形式主义类型坚决反对形而上学。
这种直率的具体形式主义似乎面临着无法克服的问题：例如，“具体不可决定”的形式，那些在与古德曼和奎因的名义主义相关的上述短论文中提到的具有不可行的长证明或证伪。韦尔试图解决这些问题，以一个相当普遍的“后弗雷格”或“新弗雷格”语言观点为基础。至少在他职业生涯的早期，弗雷格认为一个句子的真值由两个因素决定，即句子的意义、字面意义或信息内容（Sinn）和世界的状态。他最初认为，指示性和更广泛的上下文相对性可以通过假设发出和理解这些句子的说话者将它们视为更完整的句子的省略形式来满足，这些句子的意义与世界相结合，确定了唯一的真值。
后来的研究（包括弗雷格自己的研究）揭示了这种观点的不足，揭示了一些指示性在约翰·佩里的说法中是“必要的”，以表达出的思想。我可以真实地说“现在很热”，而不知道我在哪里、什么时候，甚至是谁（如果我足够迷失或失去理智）。那些不完全怀疑意义系统化理论的人，如激进的语境主义者，将弗雷格的观点修正为三分之一的观点。在特定的语境中，一个句子的真值由其信息内容、与言语相关的语境环境以及与思维和语言无关的世界共同决定。语境环境不一定出现在言语的意义或信息内容中；因此，对它们的说明可能包括日期和地点，尽管这不是“现在很热”的意义的一部分（参见卡普兰的角色与内容区分，特别是他在 1989 年（注 28：503）中讨论的第二个意义）。
这幅图片反过来暗示了这样一个观点：在特定的系统中，“使之成为真实”的背景环境与独立的现实相结合，可能以一种非现实主义的方式使其成为真实。在 Weir 对游戏形式主义的版本中，其基本思想是，在一个特定的系统中，使得“sin2θ+cos2θ=1”成为真实（或假）的原因是存在一个具体的证明或反驳，尽管这样一个具体的证明存在的陈述并不是该主张的字面意义或感觉的一部分。
这种形式主义的优点在于，它不仅肯定了数学表述的意义和具有意义的性质；与传统的游戏形式主义形成鲜明对比的是，它认为这样的表述具有真值，只要存在证明或反驳。如果能够像 Goodman 和 Quine 1947 年那样，给出一个非数学的具体证明解释，那么元理论的问题就得到了解决。当然，正如上面所提到的，仍然存在严重的问题。必须通过提供保守扩展证明等方式来解决适用性的问题。当然，这个理论不仅受到哥德尔式的不完备性和不可判定性的威胁，还受到直观真值句子的威胁；更加毁灭性的不确定性出现在“具体不可判定”句子中，比如 Tennant 在第 5 节中的素性主张。
处理这些问题的一种策略是将形式主义与严格有限主义相结合（其中一种品牌见 Yessinin-Volpin（1961；1970），以及对其的批评和评论 Dummett（1975）和 Wright（1982））：只有可行长度的“可消化”标记存在，包括公式和证明。没有可行证明或证伪的公式简单地缺乏真值。由于我们从哥德尔式的加速考虑中知道，对于许多可证明的句子来说，它或其否定的最短推导远远长于句子本身，这种有限主义/形式主义的立场威胁到了大片区域的完全普通的数学。
Weir（2010；2016）认为有限主义形式主义不仅极端，而且不连贯。原因在于缩写的普遍作用，它生成复杂的标记，其中大部分子部分将永远不存在，例如创建命名（与柏拉图主义者说话）任意高数字的缩写。结果，严格的有限主义规范不能以通常的归纳方式给出，作为包含基本集合并在复杂性形成操作下封闭的所有归纳集合的交集。而这反过来意味着我们甚至不能证明关于 wffs 和证明的非常简单的事实。
理想化在元数学中是必不可少的，包括元数学中的真理和证明的理想化概念。如果形式主义者有权主张存在无限多个质数，同时否认抽象对象的存在，那么似乎没有理由她不能肯定存在无限多个公式或无限多个证明，同时否认抽象对象的存在。因此，Weir（2016：38-39）认为，只要存在关于形式真理与形式可证性相一致的给定语言或子语言的形式真理的具体证明（或证明草图），形式主义者就可以回答具体不可判定性的问题，并且没有理由将理想化限制在有限语言上。
总之，主张标准数学理论的形式主义者，包括证明理论等，比经典游戏形式主义者拥有更多资源来满足这些要求。问题是，这些资源是否足以挽救一个公平地说，大多数数学哲学家仍然认为是绝望的立场。另一方面，对于形式主义是否已经死亡和埋葬，以及一些数学家和计算机科学家对形式主义的强烈同情的迹象，肯定没有普遍的共识。
Bibliography
Awodey, Steve, 2014, ‘Structuralism, Invariance, and Univalence’, Philosophia Mathematica (III), 22: 135–159.
Azzouni, Jody, 2004, ‘The Derivation-Indicator View of Mathematical Practice’, Philosophia Mathematica, (III) 12: 81–105.
–––, 2005, ‘How to Nominalize Formalism’, Philosophia Mathematica (III), 13: 135–159.
–––, 2006, Tracking Reason: Proof, Consequence and Truth, Oxford: Oxford University Press (especially Chapter 7).
–––, 2009, ‘Why do Informal Proofs Conform to Formal Norms’, Foundations of Science, 14: 9–26.
Barendregt, H.P., 1984, The Lambda Calculus, Amsterdam: North Holland.
Boolos, George, 1987, ‘A Curious Inference’, Journal of Philosophical Logic, 16: 1–12; reprinted in George Boolos, Logic, Logic and Logic Cambridge, MA: Harvard University Press, 1998, 376–82.
Black, M. and Geach, P, 1980, Translations from the Philosophical Writings of Gottlob Frege, Oxford: Blackwell, 3rd edition.
Carnap, Rudolf, 1934 [1937], Logische Syntax der Sprache, Vienna: Springer; translated by A. Smeaton as The Logical Syntax of Language, London: Kegan, Paul, Trench, Trubner & Co. 1937.
–––, 1950/1956, ‘Empiricism, Semantics and Ontology’, Revue Internationale de Philosophie, 4: 20–40; reprinted in Meaning and Necessity, Chicago: University of Chicago Press, 2nd edition, 1956: 205–221.
Church, Alonzo, 1932, ‘A Set of Postulates for the Foundation of Logic’, Annals of Mathematics, 33(2): 346–366.
–––,1940, ‘A Formulation of the Simple Theory of Types’, Journal of Symbolic Logic, 5(2): 56–68.
Cohen, Paul, 1971, ‘Comments on the foundations of set theory’, in Dana Scott (ed.), Axiomatic Set Theory: Proceedings of Symposia in Pure Mathematics (Volume 13), Providence: American Mathematical Society: 9–15.
Curry, Haskell, 1951, Outlines of Formalist Philosophy of Mathematics, Amsterdam: North Holland.
Curry, Haskell and Feys, Robert, 1958, Combinatory Logic, Amsterdam: North Holland.
Detlefsen, Michael, 1993, ‘Hilbert’s Formalism’, Revue Internationale de Philosophie, 47(186): 285–304.
–––, 2005, ‘Formalism’, in Stewart Shapiro (ed.), The Oxford Handbook of Philosophy of Mathematics and Logic, Oxford: Oxford University Press, 236–317.
Dummett, Michael, 1975, ‘Wang’s Paradox,’ Synthese, 30(3/4): 301–324 reprinted in Truth and Other Enigmaas London: Duckworth, 248–268.
–––, 1991, Frege, Philosophy of Mathematics, London: Duckworth.
Field, Hartry, 1989, Realism, Mathematics and Modality, Oxford: Blackwell.
Floyd, Juliet, 2002, ‘Number and Ascriptions of Number in Wittgenstein’s Tractatus’, in From Frege to Wittgenstein: Perspectives on Early Analytic Philosophy, Erich H. Reck (ed.), Oxford: Oxford University Press, 308–352.
Floyd, Juliet and Putnam, Hilary, 2000, ‘A Note on Wittgenstein’s ‘Notorious Paragraph’ about the Gödel Theorem’, Journal of Philosophy, 97: 624–632.
Frege, Gottlob, 1903, Grundgesetze der Arithmetik, Begriffsschriftlich Abgeleitet (Volume II), Jena: Pohle; reprinted 1962, Hildesheim: George Olms.
–––, 1903/1980, ‘Frege Against the Formalists: Vol II of Frege 1903, §§86–137 in Black and Geach (1980): 162–213.
–––, 1903/2013, Basic Laws of Arithmetic, edited and translated by Philip A. Ebert and Marcus Rossberg, Oxford: Oxford University Press.
Gabbay, Michael, 2010, ‘A Formalist Philosophy of Mathematics, Part I: Arithmetic’, Studia Logica, 96: 219–238.
Giaquinto, Marcus, 2002, The Search for Certainty, Oxford: Clarendon. (See especially 210ff).
Gödel, Kurt, 1953–9, ‘Is Mathematics Syntax of Language’, in S. Feferman et al. (eds.), Kurt Gödel: Collected Works (Volume III), New York: Oxford University Press, 1995: 334–362,
Goldfarb, Warren, 1995, ‘Introduction to Gödel’s ‘Is Mathematics Syntax of Language’’ in S. Feferman et al. (eds.), Kurt Gödel: Collected Works (Volume III), New York: Oxford University Press, 1995: 324–34.
Goodman, Nelson and Quine, W. V., 1947, ‘Steps towards a Constructive Nominalism’, Journal of Symbolic Logic, 12: 97–122.
Griffin, Timothy, 1990, ‘A Formulae–as–Types Notion of Control’, in Principles of Programming Languages, Association of Computing Machinery, 47–58.
Hintikka, Jaakko, 1956, ‘Identity, variables, and impredicative definitions,’ Journal of Symbolic Logic, 21: 225–45.
Howard, W.A., 1969, ‘The Formula-as-Types Notion of Construction’, in Seldin, J.P. and Hindley, J.R. (eds.) To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, London: Academic Press, 1980: 479–490.
Hylton, Peter, 1997 ‘Functions, Operations and Sense in Wittgenstein’s Tractatus’, in W.W. Tait (ed.), Early analytic philosophy: Frege, Russell, Wittgenstein: essays in honor of Leonard Linsky, Chicago: Open Court: 91–106.
Kaplan, David, 1989, ‘Demonstratives’, in J. Almog, J. Perry, and H. Wettstein (eds.), Themes from Kaplan, New York: Oxford University Press, 481–563.
Kleene, Stephen, and Rosser, J.B., 1935, ‘The Inconsistency of Certain Formal Logics’, Annals of Mathematics, 36: 630–636.
Landini, Gregory, 2007, Wittgenstein’s Apprenticeship with Russell, Cambridge: Cambridge University Press.
Lawrence, Richard, 2023, ‘Frege, Thomae, and Formalism: Shifting Perspectives’, Journal for the History of Analytic Philosophy, 11: 1–23.
Leng, Mary, 2010, Mathematics and Reality, Oxford: Oxford University Press.
Lewy, Casimir, 1967, ‘A note on the text of the Tractatus’ Mind, 76: 416–423.
Martin-Löf, Per, 1975, ‘An intuitionistic theory of types: Predicative part’, in Logic colloquium ’73, H.E. Rose and J. Shepherdson (eds.), Amsterdam: North-Holland: 73–118.
Potter, Michael, 2000, Reason’s Nearest Kin, Oxford: Oxford University Press; see especially 10–17 and Chapter 6.
Resnik, Michael, 1980, Frege and the Philosophy of Mathematics, Ithaca: Cornell University Press, 1980.
Robinson, Abraham, 1965, ‘Formalism’ in Bar-Hillel et al. (eds.) Logic, Methodology and Philosophy of Science, Amsterdam: North Holland.
–––, 1969, ‘From a Formalist’s point of view’, Dialectica, 23: 45–9.
Scott, Dana, 1970, ‘Constructive Validity’, in Symposium on Automatics Demonstration (Versailles, December 1968), M. Laudet, D. Lacombe, L. Nolin, and M. Schützenberg (eds), Lecture Notes in Mathematics (Volume 125), Berlin: Springer, 237–275.
Shapiro, Stewart, 2000, Thinking about Mathematics, Oxford: Oxford University Press.
Simons, Peter, 2009, ‘Formalism’ in Andrew D. Irvine (ed.), Philosophy of Mathematics, Amsterdam: North Holland: 291–310.
Tennant, Neil, 1997, The Taming of the True, Oxford: Clarendon Press.
–––, 2008, ‘Carnap, Gödel, and the Analyticity of Arithmetic’, Philosophia Mathematica, 16: 110–12.
Thomae, Johannes, 1898, Elementare Theorie der analytischen Functionen einer complexen Veränderlichen, 2nd edition. Halle: Verlag von Louis Nebert.
Wadler, Philip, 2015, ‘Propositions as Types’, Communications of the Association for Computing Machinery, 58: 75–84.
Wehmeier, Kai, 2004, ‘Wittgensteinian Predicate Logic’, Notre Dame Journal of Formal Logic, 45: 1–11.
Weir, Alan, 1991, ‘An Instructive Nominalism’: Critical Review of H. Field: Realism, Mathematics and Modality, Philosophical Books, 32: 17–26.
–––, 1993, ‘Putnam, Gödel and Mathematical Realism’, International Journal of Philosophical Studies, 1: 255–285.
–––, 2010, Truth through Proof: A Formalist Foundation for Mathematics, Oxford: Oxford University Press.
–––, 2016, ‘Informal Proof, Formal Proof and Formalism’, The Review of Symbolic Logic, 9: 23–43.
Wittgenstein, Ludwig, 1921/1960, Tractatus Logico-Philosophicus, D. Pears and B. McGuinness (trans.), London: Routledge and Kegan Paul.
–––, 1956/1978, Remarks on the Foundations of Mathematics, revised edition, G. E. M. Anscombe (trans.), G. E. M. Anscombe, R. Rhees, and G. H. von Wright, (eds.), Oxford: Blackwell.
–––, 1975, Philosophical Grammar, A. Kenny (trans.), Rush Rees (ed.), Oxford: Blackwell.
Wright, Crispin, 1982, ‘Strict Finitism’, Synthese, 51: 203–282.
Yessenin-Volpin, A., 1961, ‘Le Programme Ultra-Intuitionniste Des Fondements Des Mathématiques.’ in Infinitistic Methods, Proceedings of the Symposium on the Foundations of Mathematics, Oxford: Pergamon Press, 201–23.
–––, 1970, ‘The Ultra-Intuitionistic Criticism and the Antitraditional Program for the Foundations of Mathematics’, in A. Kino, J. Myhill, & R. Vesley (eds.), Intuitionism and Proof Theory, Amsterdam: North-Holland, 3–45.
Academic Tools
Look up topics and thinkers related to this entry at the Internet Philosophy Ontology Project (InPhO). | |
Enhanced bibliography for this entry at PhilPapers, with links to its database. |
Other Internet Resources
‘Does mathematics need a philosophy?’, by mathematician Timothy Gowers who presents a highly formalistic approach to mathematics
[Please contact the author with further suggestions.]
Related Entries
Frege, Gottlob: controversy with Hilbert | Gödel, Kurt | Hilbert, David: program in the foundations of mathematics | mathematics, philosophy of | mathematics, philosophy of: fictionalism | mathematics, philosophy of: Platonism | Wittgenstein, Ludwig: philosophy of mathematics
Acknowledgements
Many thanks to John L. Bell, Richard Lawrence and the editors of the Stanford Encyclopedia for very helpful feedback.
最后更新于
