组合逻辑（一）_数学联邦政治世界观

组合逻辑（以下简称 CL）是一种优雅而强大的逻辑理论，它与逻辑学的许多领域息息相关，并在其他学科中得到广泛应用，尤其是在计算机科学和数学领域。

CL 最初是作为经典一阶逻辑 (FOL) 中将逻辑常数集约化为单例集的延续而发明的。CL 解决了代换问题，因为可以通过插入组合子来准备用于消去绑定变量的公式。从哲学角度来说，没有绑定变量的表达式表示原始公式的逻辑形式。有时，绑定变量被认为表示“本体论承诺”。 CL 的另一个哲学作用是展现理论本体论假设的可变性。

代换不仅在一阶逻辑中是一项关键运算，在高阶逻辑以及其他包含变量绑定算子的形式化系统（例如 λ 演算和 ε 演算）中也是如此。事实上，在 λ 演算和与之密切相关的函数式编程语言中，正确地执行代换尤为重要。尽管 CL 没有变量绑定算子，但它可以模拟 λ 抽象。这使得 CL 成为函数式编程语言的理想编译目标语言。

与 λ 演算的联系可能正确地表明 CL 具有足够的表达能力来形式化递归函数（即可计算函数）和算术。因此，CL 容易受到哥德尔型不完备定理的影响。CL 是一个典型的术语重写系统 (TRS)。这些系统包含广泛的形式演算，从编程语言的句法规范和上下文无关语法到马尔可夫算法；甚至一些数论问题也可以看作是 TRS 问题的特殊情况。一些最初为 CL 发明的概念和证明技术，后来被证明在应用于不太理解的 TRS 时很有用。

CL 通过类型化与非经典逻辑相联系。首先，发现了直觉逻辑蕴涵片断中可证明的公式与可类型化的组合项之间的对应关系。随后，同构被推广到其他组合基和蕴涵逻辑（例如相关蕴涵逻辑、指数自由线性逻辑、仿射逻辑等）。

自指因素导致了某些悖论，例如广为人知的说谎者悖论和罗素悖论。集合论对函数的理解也阻碍了函数的自应用。因此，值得注意的是，纯无类型逻辑集合论 (CL) 并不排除函数的自应用。此外，它的数学模型表明，函数可以成为自身参数的理论除了具有一致性之外，还完全合理（这一点先前已使用证明论方法确立）。

1. 申芬克尔 (Schönfinkel) 的边界变量消去

1.1 代换问题

1.2 运算符“nextand”和“U”

1.3 替代方法：基本逻辑和谓词函子

2. 组合项及其主要性质

2.1 归约、相等及其形式化

2.2 丘奇-罗瑟定理和一致性定理

2.3 不动点的存在性和组合完备性

3.非经典逻辑和类型化逻辑逻辑

3.1 简单类型

3.2 交叉类型

4. 模型

4.1 斯科特模型

4.2 关系语义

5. 可计算函数和算术

5.1 哥德尔句子

参考文献

学术工具

其他网络资源

相关条目

1. 申芬克尔的边界变量消去

1.1 代换问题

经典的一阶逻辑包含量词，分别用∀（“对于所有”）和∃（“存在”）表示。诸如“所有鸟类都是动物”这样的简单句子可以形式化为∀x(Bx⊃Ax)，其中x是变量，B和A是单项谓词，⊃是（实质）蕴涵的符号。闭公式∀x(Bx⊃Ax)中的变量是绑定的，而开公式Bx⊃Ax中的变量是自由的。假设t（代表“Tweety”）是一个名称常量，那么上述句子的一个实例就是Bt⊃At，可以理解为“Tweety是一种动物，前提是Tweety是一只鸟”。这说明（全称）量词的实例化涉及代换。

由于示例简单，在Bx和Ax中用t代换x似乎很容易理解和执行。然而，对于FOL（以及一般而言，对于抽象语法，即具有变量绑定运算符的语言）的代换定义必须保证被代换表达式中不存在任何自由出现的变量在结果表达式中成为绑定的。

为了说明可能出现的问题，我们考虑（开放）公式 ∀x(Rxy∧Rxr)，其中 R 是一个二元谓词，r 是一个缩写为“Bertrand Russell”的名称常量，∧ 是合取。∀x(Rxy∧Rxr) 包含 y 的自由出现（也就是说，y 是公式的自由变量），然而，y 不能自由地替换包含 x 的自由出现的项，例如，x 本身。更正式地讲，∀x(Rxy∧Rxr) 中 R 的第二个自变量位置上 y 的出现不受公式量词（唯一量词）的约束，而∀x(Rxx∧Rxr) 是一个封闭公式，也就是说，它不包含变量的自由出现。非正式地讲，以下自然语言句子可以被认为是对前几个公式的解释。“Everybody reads him and Russell,”（其中“him”是指示词，或者可能是照应词）和“Everybody reads themselves and Russell”。显然，即使我们假设每个人都写点什么，这两句话的含义也大不相同。相比之下，∀x(Rxw∧Rxr) 表现出用名称常数 w 代替 y 的自由出现的无问题替代。（后一个公式或许形式化了“每个人都读路德维希·维特根斯坦和伯特兰·罗素”这句话。）这些例子旨在说明摩西·申芬克尔着手解决的问题中更复杂的部分，以及他发明逻辑推理（CL）的目的。[1]

1.2 运算符“nextand”和“U”

关于经典句子逻辑（SL）的一个著名结果是，所有真值函数都可以用¬和∧（或¬和∨等）来表示。然而，最小充分连接词集只能包含一个连接词，例如∣（“nand”，通常被称为谢弗的笔触）或↓（“nor”，即皮尔斯的联合否定）。“Nand”是“非与”，换句话说，A∣B 定义为¬(A∧B)，其中 A、B 遍历公式，¬ 为否定。反过来，如果∣是原语，则¬A可定义为A∣A，A∧B可定义为(A∣B)∣(A∣B)。虽然包含大量竖线的公式可能很快在视觉上变得混乱且难以解析，但很容易证明，仅凭∣就足以表达所有真值函数。申芬克尔的目标是最小化 FOL 形式化所需的逻辑常量数量，就像亨利·M·谢弗（实际上，查尔斯·S·皮尔斯早已是）对经典命题逻辑所做的那样。上述两个量词中，一个是充分的，另一个可以假定已定义。假设∃xA 是 ¬∀x¬A 的缩写。即使将 ¬ 和其他连接词替换为 ∣，仍然有两个逻辑常量：∀ 和 ∣。另一个紧迫的问题是量词可以嵌套（即，一个量词的作用域可能完全包含另一个量词的作用域），并且变量绑定（可以通过在量词和它们绑定的变量之间画线来可视化）可能会变得非常复杂。暂且保留我们熟悉的逻辑常数，我们来看看下面的公式，它暗示了在全面考虑待解决的问题时出现的困难。[2]

∀x(∃y(Py∧Bxy)⊃∃y(Py∧Bxy∧∀z((Rz∧Ozy)⊃¬Cz)))

∀x 绑定所有出现的 x；两个 B 的第二个参数处的变量由两个 ∃y 中的一个绑定，后者通过 Ozy 与 ∀z 交互。

在 FOL 中，谓词具有固定的有限元数，并且没有任何规则可以同时绑定一个谓词的第一个参数和另一个谓词的第二个参数中的变量。（事实上，如果排除这种绑定而没有某种补偿手段，FOL 会失去部分表达能力。）当一个公式被转换成一个（等价的）前缀范式公式时，这些困难仍然存在。只要变量绑定可以交织成任意复杂的模式，似乎就没有办法消除绑定变量。（请注意，开放公式中的自由变量——在某种意义上——表现得像局部名称常量，它们的消除既不是有意为之，也没有在本文描述的过程中实现。）

Schönfinkel 的独创性在于他引入了组合子来解开变量绑定。组合子 S、K、I、B 和 C（以当代符号表示）是他提出的，并且他确定 S 和 K 足以定义所有其他组合子。实际上，他还定义了一种执行绑定变量消除的算法，这本质上是当今在 CL 中定义括号抽象的算法之一。[3]

Schönfinkel 引入了一个新的逻辑常量 U，它表示两个类的不相交性。例如，当 P 和 Q 是单元谓词时，UPQ 可以用通常的 FOL 符号写成 ¬∃x(Px∧Qx)。（例如，该公式可以被认为是对自然语言句子“没有鹦鹉是安静的”的形式化。）在消除绑定变量的过程中，UXY 由包含“Xx”和“Yx”的表达式获得，其中 x 不出现在 X 或 Y 中。例如，如果 X 和 Y 恰好是 n 元谓词，且 n≥2，则 x 仅出现在它们的最后一个参数处。“没有人读亚里士多德和柏拉图”可以形式化为 ¬∃x(Rxa∧Rxp)，其中 a 和 p 分别是代表“亚里士多德”和“柏拉图”的名称常量。该公式不能写成 U(Ra)(Rp)。另一方面，“没有一个人同时被罗素和维特根斯坦读过”，也就是说，¬∃x(Rrx∧Rwx) 变成了 U(Rr)(Rw)，其中括号描述了 U 的参数。通常，表达式 X 和 Y（在 UXY 中）由谓词（和名称常量）以及组合子和其他 U 组成。

“下一个”的符号很有用（即，“不存在与”（not-exists-and），无需假设 x 在连接的表达式中可以自由出现，也无需假设如果 x 存在，那么它是表达式的最后一个组成部分。遵循 Schönfinkel 的思想，我们用 ∣x 表示绑定 x 的“下一个项”运算符。（符号 ∣− ，其中 − 是变量的位置，与 Sheffer 笔画非常相似。）Schönfinkel 实现了将 FOL 的逻辑常量集简化为单例集 {∣−} 的目标，因为 FOL 的每个公式都等价于一个只包含“下一个项”的公式。

即使 A 中没有 x 的自由出现，公式 ∀xA 通常也被定义为在 FOL 中合式的。那么，当然，∀xA 等价于 A 以及 ∃xA，这样的量词被称为空的。为了证明任何公式都可以重写成仅包含“下一个项”的等价公式，只需检查以下 Schönfinkel 对 ¬、∨ 和 ∀ 的定义（使用合适的变量）即可。

¬A ⇔dfA∣xA

A∨B ⇔df(A∣yA)∣x(B∣yB)

∀xAx ⇔df(Ax∣yAx)∣x(Ax∣yAx)

例如，¬ 的定义可以通过以下等价关系得到证明。A⇔A∧A，A∧A⇔∃x(A∧A)（假设 x 在 A 中不为自由元素），因此，通过替换，¬A⇔¬∃x(A∧A)。

现在我们举一个具体的例子来说明如何将 FOL 公式转化为仅包含∣−的公式，以及如何使用 U 和组合子消去绑定变量。为了使这个过程更有趣，我们从 (1)：中的句子开始。

(#1)

每个自然数都有一个更大的素数。

这句话的一个直接形式化——在数论的前沿——是 (2)：中的公式（其中，“Nx”代表“x 是自然数”，“Px”代表“x 是素数”，“Gxy”读作“x 大于 y”）。(#2)

∀y∃x(Ny⊃(Px∧Gxy))

此公式等价于∀y(Ny⊃∃x(Px∧Gxy))，进而等价于¬∃y¬(Ny⊃∃x(Px∧Gxy))。再经过一两步，我们得到Ny∣y(Px∣xGxy)。（除非括号另有说明，否则表达式均视为向左分组。例如，Gxy 是 ((Gx)y) 而不是 G(xy)，这或许是基于 FOL 公式中最常见的括号排列方式而得出的。）遗憾的是，在最后一个表达式中，∣x 和 ∣y 都不能被 U 替换。但是，如果对 G 的参数进行置换，则可以执行前面的归约。其中一个组合子 C 恰好满足了我们的需求：Gxy 可以转换为 CGyx（参见 2.1 节中组合子的定义）。也就是说，我们有 Ny∣y(Px∣xCGyx)，然后是 Ny∣yUP(CGy)。[4] 该表达式可能给人的印象是 y 是 UP(CGy) 的最后一个分量，而 UP(CGy) 是 ∣y 的第二个参数，但事实并非如此。表达式中的分组不能被忽略，需要另一个组合子 B 将 UP(CGy) 转换为所需的形式 B(UP)(CG)y。从 Ny∣yB(UP)(CG)y，我们再一步就可以得到 UN(B(UP)(CG))。这个表达式完全没有变量，也使得 FOL 中绑定变量的重命名变得更容易理解：给定两个前两个元素不同的（不同）变量序列，上述过程的逆过程将得到公式，它们是 (2)：中公式的（逻辑上等价的）字母变体。

与 FOL 公式相比，表达式 UN(B(UP)(CG)) 可能看起来“陌生”，但符号——在很大程度上——是一种约定俗成的表达方式。值得注意的是，第一个 U 后面跟着它的两个参数，而第二个 U 后面不是。B(UP) 是子表达式，但 UP(CG) 不是 UN(B(UP)(CG)) 的子表达式。此外，整个表达式可以使用组合子转换为 XNPG，其中 X 仅由 U 和组合子组成。这样的 X 简洁地编码了公式的逻辑形式或逻辑内容，谓词作为参数。[5]

通过上述转换获得的表达式很快就会变得冗长——就像尝试重写一个简单的 FOL 语句（例如 ∃x(Px∧Qx)）一样。[6] 然而，这并没有降低 Schönfinkel 理论结果的重要性。表达式长度的轻微增加（如果有的话）甚至不会造成不便，更不用说在拥有 PB 级（甚至是 EB 级和 ZB 级）内存的计算机时代会造成阻碍了。

尽管 Wolfram (2020) 最近发表了论文，但 Schönfinkel 的 FOL 简化程序却鲜为人知，这似乎令人遗憾。本书旨在纪念Schönfinkel讲座（他在该讲座中引入了组合子）发表一百周年，本书通过计算机辅助探索组合子领域，并引用文献填补了历史背景中的空白。为了衡量Sheffer和Schönfinkel的归约广为人知，我们援引了这样一个事实：Sheffer是标准逻辑入门课程的一部分，而Schönfinkel则不是。毫无疑问，其中一个原因是Schönfinkel消去绑定变量的过程在概念上比从∣（或↓）定义几个真值函数更为丰富。另一个原因可能是Schönfinkel可能没有足够强调允许通过“nextand”消去所有其他逻辑连接词和量词的中间步骤。Schönfinkel论文英译本的引言也忽略了这一步骤的重要性。这篇文章写于原版发表30多年后。我们还可以注意到，尽管“nextand”在标准逻辑意义上是一个运算符，但它是二元的——不像∀和∃那样是一元的。

如果将 A∣B⇔df¬(A∧B) 作为定义添加到 SL，则结果是一个保守的扩展，并且可以证明：对于任何公式 A(p0,…,pn)（即包含所示命题变量和一些连接词的公式），存在一个仅包含连接词∣的公式 B(p0,…,pn)，并且 B(p0,…,pn)⇔A(p0,…,pn) 本身是可证明的。∣当然被解释为“与非”真值函数。 “Nand” 作为二元连接词或二元真值函数，其对象类型与合取、析取等类似。

Schönfinkel 对 FOL 扩展的第一阶段与此类似。∣− 的添加（也）是 FOL 的保守扩展，并且所有出现的 ∣− 都可以被消除。（我们注意到 ∣− 是一个二元运算符，因此它可以被认为是将量词 (∃) 与连接词 (¬, ∧) 组合在一起，但 ∣− 当然不会引入任何在 FOL 中无法定义的对象。）

Schönfinkel 对 FOL 扩展的第二阶段略有不同。UXY 仅在单元谓词 P 和 Q 中可定义（或当其最后一个参数中的变量被绑定时，对于元数更高的谓词）。因此，一般而言，U 和组合子在 FOL 中均不可定义。

绑定变量的消除超出了 FOL 的资源范围。组合子不仅不可定义，而且是 FOL 本身所不具备的新对象类型。此外，绑定变量消除过程的中间步骤预设了多参数函数可以视为单参数函数，反之亦然。[7] 用具有足够多且顺序正确的参数的谓词字母来丰富 FOL 的表示形式，这或多或少不会有问题，而且它会为语言添加与其他谓词具有相同解释类型的对象。然而，一个潜在的问题是，对于每个谓词，都需要无限多（ℵ0 个）新的谓词，以及规定谓词变体含义之间预期等价关系的公理。从符号上讲，这些步骤相当于用额外的参数填充谓词符号，省略一些参数，以及对参数进行排列和重组。尽管其中一些添加可能看起来多余或过于繁琐，但为了理解 Schönfinkel 消除绑定变量的程序，必须注意到公式被视为结构化的符号字符串。[8]

总结本节，需要强调的是，上述约简过程不存在一致性问题，因为它可以被看作——或者用当代术语来描述——一个定义明确的算法。如果我们考虑用组合子扩展的FOL语言，那么得到的系统是不一致的，这完全是另一回事，因为CL足够强大，可以定义任何函数的不动点。所有函数（包括真值函数）都拥有不动点的效果，可以理解为将某些双条件句（可能有效也可能无效）添加为公理。（例如，罗素悖论源于否定联结词的不动点。）值得注意的是，FOL和（纯）CL都是一致的。

1.3 替代方法：基本逻辑和谓词函子

本节将简要概述两种与申芬克尔的工作相关或受其在消除绑定变量中使用组合子启发的思想。

菲奇的元逻辑

从20世纪30年代末开始，弗雷德里克·菲奇致力于研究一种他称之为基本逻辑的逻辑。这一称谓源于他旨在提供一个框架，使任何逻辑都能形式化。菲奇的方法完全是句法的（与申芬克尔的方法非常相似），而“形式化”应理解为将一个形式描述的系统编码到另一个系统中——这与哥德尔不完备定理中句法的算术化类似。

1942年，菲奇引入了一种他称之为K的逻辑。K中的表达式像组合项一样，由二元应用运算构成，而该运算不被假设为具有结合律。（参见下一节中组合术语的定义。）然而，K 的常数与纯 CL 的常数并不一致。Fitch 使用了 10 个常数：ε、o、

、

、W、=、∧、∨、E 和 ∗。前五个常数是组合子，尽管其符号可能暗示不同的（非正式的）含义。“=”表示表达式的句法身份。“∧”和“∨”分别代表“与”和“或”。“E”类似于申芬克尔的 U，但它对应于非空的存在量词。最后，“∗”类似于二元关系的传递闭包运算符或克莱尼星。值得注意的是，该系统中没有否定或全称量词。这些常数的用法具有如下特征——有点像公理表征组合子。=ab 当且仅当 a 和 b 在语法上是相同的表达式

εab 当且仅当 ba

oabc 当且仅当 a(bc)

abc 当且仅当 bac

abcd 当且仅当 a(bc)d

Wab 当且仅当 abb

∧ab 当且仅当 a 且 b

∨ab 当且仅当 a 或 b

Eb 当且仅当 ∃a.ba

∗abc 当且仅当 abc 且 ∃d.abd&adc

在逻辑推理中，公理后面紧接着诸如单步和弱归约之类的概念，后者可以被视为计算或推理步骤。（有关这些概念的部分内容，请参阅下一节。）类似地，例如，用于逻辑推理的公理演算除了公理之外，还包含推理规则。理解各种基本逻辑表述方式的障碍之一是缺乏相似的表述方式。

（本章完）