组合逻辑（二）

与 FOL 的公式相比，表达式 UN(\textsf{B}(UP)(\textsf{C}G)) 可能看起来“陌生”，但符号在很大程度上是一个约定问题。有趣的是，第一个 U 后面只是简单地跟随了它的两个参数，但是第二个 U 则不然。 \textsf{B}(UP) 是子表达式，但 UP(\textsf{C}G) 不是 UN (\textsf{B}(UP)(\textsf{C}G)) 的子表达式。此外，整个表达式可以使用组合子转换为 XNPG，其中 X 仅由 Us 和组合子组成。这样的 X 简洁地编码了以谓词为参数的公式的逻辑形式或逻辑内容。 [5]

通过上述转换获得的表达式很快就会变得冗长——正如尝试重写一个简单的 FOL 句子（例如 \exists x(Px\land Qx) 所示）所示。[6]然而，这并没有削弱舍恩芬克尔理论结果的重要性。表达式长度的轻微增加（如果有的话）甚至不会带来不便，更不用说在拥有拍字节（甚至艾字节和泽字节）内存的计算机时代成为障碍。

不幸的是，尽管最近出版了 Wolfram (2020)，但 Schönfinkel 的 FOL 缩减程序并未广为人知。本书是为了庆祝 Schönfinkel 演讲（他在演讲中介绍了组合器）100 周年而编写的，书中对组合器领域进行了计算机辅助探索，并用文档填补了历史背景中的空白。作为衡量谢弗和舍恩芬克尔的归约广为人知的标准，我们诉诸这样一个事实：第一个是逻辑学标准入门课程的一部分，而第二个不是。毫无疑问，原因之一是 Schönfinkel 消除绑定变量的过程在概念上比从 \mid （或 \downarrow）定义一些真值函数更加丰富。另一个原因可能是舍恩芬克尔没有足够重视中间步骤，该步骤允许通过“nextand”消除所有其他逻辑连接词和量词。 Schönfinkel 论文的英文译本的介绍中也忽略了这一步的重要性，该论文是在原始发表 30 多年后撰写的。我们还可能注意到，虽然“nextand”是标准逻辑意义上的运算符，但它是二元的——与一元的 \forall 和 \exists 不同。

如果 A\mid B \Leftrightarrow_\textrm{df} \lnot(A\land B) 作为定义添加到 SL 中，则结果是保守扩展，并且可证明对于任何公式 A(p_0,\ldots ,p_n) （即，对于包含显示的命题变量和一些连接词的公式），有一个仅包含连接词 \mid 的公式 B(p_0,\ldots,p_n) 和 B(p_0,\ldots,p_n)\Leftrightarrow A(p_0,\ldots,p_n) 本身是可证明的。 \mid 当然被解释为“nand”真值函数。 “Nand”作为二元联结词或二元真值函数，与合取、析取等属于同一类对象。

Schönfinkel 扩展 FOL 的第一阶段是类似的。添加 \mid^- 也是 FOL 的保守扩展，并且可以消除每次出现的 \mid^- 。 （我们注意到\mid^-是一个二元运算符，因此可以认为将量词（\exists）与连接词（\lnot，\land）组合起来，但是\mid^-当然不会引入任何对象FOL 中无法定义。）

Schönfinkel 扩展 FOL 的第二阶段略有不同。 UXY 在 FOL 中只能定义为一位谓词 P 和 Q（或者当最后一个参数中的变量被绑定时，对于更高数量的谓词）。因此，一般来说，U 和组合子都无法在 FOL 中定义。

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

在本节的结论中，重要的是要强调，上述归约过程不存在一致性问题，因为它可以被视为（或用当代术语描述）为一种定义明确的算法。这是一个完全不同的问题，如果我们考虑使用组合器扩展的 FOL 语言，那么生成的系统是不一致的，因为 CL 足够强大，可以定义任何函数的不动点。所有函数（包括真值函数）具有不动点的效果可能被认为相当于添加某些双条件（可能有效也可能无效）作为公理。 （例如，罗素悖论是从否定联结词的固定点出现的。）值得注意的是，FOL 和（纯）CL 是一致的。

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

在本节中，我们简要概述了与 Schönfinkel 的工作相关或受他在消除绑定变量时使用组合器的启发而激发的两个想法。

惠誉的元逻辑

从 20 世纪 30 年代末开始，弗雷德里克·菲奇 (Frederic Fitch) 研究了一种他称之为基本逻辑的逻辑。该标签的动机是他的目标是提供一个可以将任何逻辑形式化的框架。菲奇的方法完全是句法的（很像舍恩芬克尔的方法），“形式化”应被理解为在另一个系统中编码形式化描述的系统——与哥德尔不完备定理中语法的算术化不同。

1942 年，Fitch 引入了一种逻辑，他将其标记为 K。K 中的表达式是通过二元应用运算形成的，类似于组合项，不假定其具有关联性。 （请参阅下一节中组合项的定义。）但是，K 的常数与纯 CL 的常数不一致。 Fitch 使用 10 个常数：\varepsilon、o、\acute{\varepsilon}、\acute{o}、W、=、\land、\lor、E 和 *。前五个常量是组合符，尽管符号可能暗示不同的（非正式）含义。 ‘=’是表达式的语法同一性。 ‘\land’ 和 ‘\lor’ 旨在代表“and”和“or”。 “E”是 Schönfinkel 的 U 的类似物，但它对应于非空的存在量词。最后，“*”类似于二元关系的传递闭包运算符或 Kleene 星。值得注意的是，该系统中没有否定或全称量词。常量的使用特征如下——有点像公理特征组合器。

=ab 当且仅当 a 和 b（在语法上）是相同的表达式

\varepsilon ab 当且仅当 ba

oabc 当且仅当 a(bc)

\acute{\varepsilon} abc 当且仅当 bac

\acute{o} abcd 当且仅当 a(bc)d

Wab 当且仅当 abb

\land ab 当且仅当 a 和 b

\lor ab 当且仅当 a 或 b

Eb 当且仅当\存在a.\,ba

*abc 当且仅当 abc 和 \存在 d.\,abd\&adc

在 CL 中，公理后面跟着诸如一步和弱约简之类的概念，后者可以被视为计算或推理步骤。 （有关其中一些概念，请参阅下一节。）类似地，例如，FOL 的公理演算除了公理之外还包含推理规则。理解基本逻辑的各种表述的障碍之一是缺乏类似的表述。

在他的第一篇关于基本逻辑的论文之后的大约二十年里，菲奇发表了一系列关于基本逻辑的论文，致力于（1）递归函数的表示（即语法算术化的可能性的演示），（ 2) K^\prime，K 的扩展，带有否定、全称量词和（*：运算符的对偶），(3) K 和 K^\prime 的一致性，(4) L，K^ 的扩展\prime 带有蕴涵和必然性运算符，(5) 一些常量的可定义性，例如 * 和 ，以及：E。

K 中包含的组合器（因此，在其所有扩展中）是 \textsf{T}、\textsf{B} 和 \textsf{W}。 \acute \varepsilon 和 \acute o 分别是 \textsf{T} 的三元版本和 \textsf{B} 的四元版本。罗素悖论涉及否定，但库里悖论（的任一变体）是正的，因为它依赖于大卫·希尔伯特的正蕴涵逻辑的一两个定理。这意味着，如果基本逻辑的各种系统，特别是 K^\prime 和 L 是一致的，那么它们要么不能包含完全的抽象，要么蕴涵、蕴涵和恒等的概念应该不同于它们通常的对应物。事实上，K、K^\prime 和 L 不是外延系统。也就是说，即使应用于同一表达式的两个表达式始终相等，所应用的表达式也不相等。事实证明，将基本逻辑转变为扩展系统并不那么简单。 Fitch 的系统 JE^\prime 被 Myhill 证明是不一致的，这导致外延同一性的条件表述更加复杂。

基本逻辑还没有成为描述形式系统的广泛使用的通用框架；然而，Updike（2010）对这种方法重新产生了兴趣，他试图将基本逻辑置于 20 世纪中叶基础工作的更广泛背景中。

蒯因的消除策略

从 20 世纪 30 年代末开始，W. V. O. Quine 致力于研究一种替代方法来消除一阶逻辑中的绑定变量。可以合理地假设，舍恩芬克尔的目标是在经典逻辑中找到单个运算符，然后消除绑定变量（正如他在舍恩芬克尔（1924）中所声称的那样），而不是定义一个总体符号系统来描述所有数学。尽管如此，CL 很快就以一种更随心所欲的方式与经典逻辑融合，从而导致了一个不一致的系统。

蒯因找到了摆脱这种情况的出路：通过隐式类型化常量（在某种程度上类似于组合器）可能会出现不一致的情况。他将此类常量称为谓词函子，并引入了其中的几组，最后一组是在 Quine (1981) 中提出的。

FOL 最常见的表示形式规定，n 处谓词后跟一系列 n 项（可能用逗号分隔并用括号括起来）是一个公式。 （这与 Schönfinkel 的公式观点相反，并且与谓词作为 n 元关系的非正式和正式解释一致。换句话说，FOL 不允许谓词或其解释的“柯里化”。）蒯因同意认为术语序列遵循谓词。

与组合器不同，谓词函子彼此不适用。这是蒯因反复强调的一点。原子谓词是一阶语言的谓词，而复杂谓词是通过将谓词函子（适当数量）应用于谓词（可以是原子的或复杂的）来获得。

禁止自应用以及使用“平面”参数序列意味着需要无限多个谓词函子来确保从 FOL 的所有公式中消除绑定变量。为了快速解释这个问题：否则无法确保一对任意相距的元素的排列。正如组合器可以根据其效果进行分组一样，蒯因能够选择可以根据其效果自然分组的谓词函子。事实上，谓词函子组与组合器类相似，尽管蒯因的标签常常是崇高的。为了给出这种替代方法的具体示例，我们概述了 Quine (1981) 的一组谓词函子的稍微修改版本。

假设一阶语言以 \mid^- 作为唯一运算符。 （F 和 G 是谓词函子语言中谓词的元变量。） \wr^n \textit{Inv}^n、\textit{inv}^n、\textit{Pad}^{n+1} 和 \textit{对于每个 n\in\omega，Ref}^n 是谓词函子。通过应用以下子句，将FOL的公式重写为谓词函子语言的公式。

FOL的变量x和谓词P在谓词函子语言中分别是x和P。

Fx_1x_2\ldots x_n\mid^{x_1}Gx_1x_2\ldots x_n \mathbin{{:}{=}{:}} (F\wr G)x_2\ldots x_n，其中 x_2,\ldots, x_n 与 x_1 不同， F 和 G 后面跟着相同的变量序列。

Fx_1x_2\ldots x_n \mathbin{{:}{=}{:}} (\textit{Inv }F)x_2\ldots x_nx_1

Fx_1x_2\ldots x_n \mathbin{{:}{=}{:}} (\textit{inv }F)x_2x_1\ldots x_n

Fx_2\ldots x_n \mathbin{{:}{=}{:}} (\textit{Pad } F)x_1x_2\ldots x_n

Fx_1x_1x_2\ldots x_n \mathbin{{:}{=}{:}} (\textit{Ref }F )x_1x_2\ldots x_n

\textit{Ref} 和 \textsf{W}、\textit{Pad} 和 \textsf{K} 以及 \textit{Inv} 和 \textit{inv} 以及具有置换效果的各种组合器之间存在明显的相似性（例如，\textsf{C} 和 \textsf{T}）。如果 \mid^- 是一阶语言中唯一的运算符，那么所有非原子公式几乎都是 2 中左侧表达式的形式。必须保证的是，侧面条件满足，这就是第 3-6 条的内容。尽管 \wr、\textit{inv}、\textit{Pad} 和 \textit{Ref} 的各种 n 元版本可以合并（通过忽略未受影响的参数），但 \textit{Inv} 显然代表无限多个谓词函子，因为 x_1,\ldots,x_n 不能被忽略或省略。

有趣的是，\wr 和 Schönfinkel's U 之间存在差异。不仅绑定变量的位置不同，而且 \wr 构建了 n-1 个变量的收缩（由 \mid^- 和 \mid^- 分隔）左侧表达式中的其他符号）。

蒯因希望谓词函子语言能够带来一种新颖的一阶逻辑代数化。虽然可以使用谓词函子消除绑定变量，但蒯因从未定义过通常意义上的代数——例如，类似于多元代数或圆柱代数。从设计上来说，谓词函子的适用性非常有限，这带来了不幸的副作用，即它们似乎没有什么意义，并且在其预期上下文之外没有太多用处。

2. 组合项及其主要性质

2.1 约简、平等及其形式化

格奥尔格·康托尔（Georg Cantor）和伯特兰·罗素（Bertrand Russell）在19世纪末20世纪初发现的悖论都涉及集合的自隶属性。阿尔弗雷德·怀特海德 (Alfred N. Whitehead) 和伯特兰·罗素 (Bertrand Russell) 提出的分支理论以及 ZF（以恩斯特·泽梅洛 (Ernst Zermelo) 和亚伯拉罕·A·弗兰克尔 (Abraham A. Fraenkel) 命名的集合论的形式化）排除了自我隶属性。然而，似乎一直渴望创建一种允许自我成员资格或自我应用的理论。事实上，库里开发 CL 的动机之一是构建一种形式语言，其中包括广泛的格式良好的表达式，其中一些表达式在某些解释下可能会变得毫无意义。 （这个想法可以与集合论的冯·诺依曼-伯内斯-哥德尔形式化相比较，其中，在没有基础公理的情况下，罗素类可以被证明不是一个集合，因此是一个真类。）

一些自然语言示例提供了一个方便的例证，可以阐明（1）之间的差异，即形式良好（但毫无意义）的表达和（2），这是一个有意义的（但不明式的）句子。 （当然，（2）的意义应与一粒盐一起使用。实际上，库尔特·戈德尔（KurtGödel Gödel在1930年证明了（2'）Peano算术的扭曲版本是不完整的。）

(1)

\ lambda x \，（x^2+4x-6）的派生词希望声明功能是智能的。

(2)

Peano算术在1930年证明与Gödel不完整。

在这些非正式动机之后，我们转向CL适当，并更加正式地介绍其一些概念。

Cl中的对象称为术语。[9]术语可能被认为被解释为功能（如第4.1节中进一步解释）。原始术语包含变量和常数，而复合项是通过组合术语形成的。通常，包括一个变量的不可变性集（即具有基数\ Aleph_0的集合），并且常数包括一些（未定义的）组合器。 （我们将x，y，z，v，w，u，u，x_0，\ ldots用作对象语言中的变量，而m，n，p，q，\ ldots作为跨越术语的metavariables。

术语的归纳定义如下。

（T1）

如果x是变量，则x是一个术语；

（T2）

如果C是常数，则C是一个术语；

（T3）

如果m和n是术语，则（MN）是一个术语。

在上面的定义中，（t3）隐藏了连接两个术语m和n的二进制操作。此操作称为应用，通常用并置表示，也就是说，通过将其两个参数相互放置，如（ MN）。

由于其预期的解释是功能应用，因此不认为应用程序具有其他属性（例如通勤性）。例如，（（vw）u）和（v（wu））是不同的术语 - 仅是\ lambda x。\，x^2+4x-6的衍生物应用于8（即（\ lambda x）。 \，2x+4）8 = 20）与90的导数（即（8^2+32-6）'= 0）不同。使用\ lambda符号，示例中的两个术语可以表示为

（（\ lambda y。\，y'）（\ lambda x。\，x^2+4x-6））8

与

（\ lambda y。\，y'）（（\ lambda x。\，x^2+4x-6）8）。

如果将项视为结构化字符串（括号显示分组），则与长度为n的字符串相关的不同项的数量是加泰罗尼亚数字C_ {N-1}。对于非阴性整数n（即，对于N \ in \ Mathbb {n}），

c_n = \ frac {1} {n+1} {2n \选择n}。

前七个加泰罗尼亚数字是C_0 = 1，C_1 = 1，C_2 = 2，C_3 = 5，C_4 = 14，C_5 = 42和C_6 = 132。作为例证，我们可能会（简单地）用X组成，因为术语仅在分组中有所不同。显然，如果该术语是x或xx，即长度为1或2的术语，则只有一种形成术语的方法，也就是说，每种情况下只有一个可能的术语。如果我们从三个XS开始，则可以形成（xx）x​​或x（xx）。如果术语的长度为4，则五个项为：xxxx，x（xx）x​​，xx（xx），x（xxx）和x（x（xx））。 （尝试列出可以从5 xs形成的14个不同术语的有用练习。）

CL中通常的符号惯例是将括号从左相关术语和最遥远的一对删除。例如，XYZ将完全写成（（xy）Z），而XY（XZ）和（XY）（XZ）都是该术语（（（XY）（XZ）））的“速记版本”（与XYXZ不同。用术语分组描述了子。例如，XY是本段中提到的每个术语的子术语，而Yz和Yx则是这些术语的奇异。

数学联邦政治世界观提示您：看后求收藏（笔尖小说网http://www.bjxsw.cc），接着再看更方便。