组合逻辑（一）

1. Schönfinkel 消除束缚变量

1.1 替代问题

1.2 运算符“nextand”和“U”

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

2. 组合项及其主要性质

2.1 约简、平等及其形式化

2.2 Church-Rosser定理和一致性定理

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

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

3.1 简单类型

3.2 交叉口类型

4. 型号

4.1 斯科特的模型

4.2 关系语义

5.可计算函数和算术

5.1 哥德尔句子

参考书目

学术工具

其他互联网资源

相关条目

1. Schönfinkel 消除束缚变量

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) 是一个封闭公式，也就是说，它不包含自由出现的变量。非正式地，以下自然语言句子可以被认为是对前面公式的解释。 “每个人都读他和罗素”（其中“他”是指示性的，或者可能是照应词）和“每个人都读他自己和罗素”。显然，即使我们假设每个人都写了一些东西，这两个句子的含义也有很大不同。相比之下，∀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)。尽管具有大量垂直线的公式可能很快就会在视觉上变得混乱且难以解析，但可以直接证明 ∣ 本身就足以表达来定义所有真值函数。

Schönfinkel 的目标是最大限度地减少 FOL 形式化所需的逻辑常数的数量，就像 Henry M. Sheffer（实际上已经是 Charles S. Peirce）对经典命题逻辑所做的那样。上述两个量词之一就足够了，另一个可以假设已定义。假设，∃xA 是 Ø∀xØA 的缩写。即使 ¬ 和其余连接词换成 ∣，仍然保留两个逻辑常数：∀ 和 ∣。另一个紧迫的问题是量词可能是嵌套的（即，一个量词的范围可能完全包含另一个量词的范围），并且变量绑定（可以通过在量词和它们绑定的变量之间画线来可视化）可能会得到相当交织在一起。暂时保持熟悉的逻辑常数，我们可以看看下面的公式，它暗示了新出现的困难——当要解决的问题被全面考虑时。 [2]

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

∀x 绑定所有出现的 x；两个 B 的第二个参数位置的变量由两个 ∃y 之一绑定，后者通过 Ozy 与 ∀z 相互作用。

FOL 中的谓词具有固定的有限数量，并且不排除在一个谓词的第一个参数和另一个谓词的第二个参数中同时绑定变量。 （事实上​​，如果这种类型的绑定被排除而没有某种方法来补偿它们，那么 FOL 将会失去一些表达能力。）当一个公式被转换成 prenex 范式的（n 等价）公式时，这些困难仍然存在。只要变量绑定可以交织并编织成任意复杂的模式，似乎就没有办法消除绑定变量。 （请注意，开放公式中的自由变量在某种意义上的行为类似于局部名称常量，并且它们的消除既不是有意的，也不是在此处描述的过程中实现的。）

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

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

使用“nextand”（即“not-exists-and”）表示法很有用，无需假设 x 在连接的表达式中自由出现，或者如果有一个，则它是的表达方式。遵循 Schönfinkel，我们使用 \mid^x 作为绑定 x 的“nextand”运算符。 （符号 \mid^-，其中 ^- 是变量的位置，与 Sheffer 笔划非常相似。）Schönfinkel 实现了将 FOL 的逻辑常量集减少到单例集 \{\mid^- \}，因为 FOL 的每个公式都相当于只包含“nextand”的公式。

公式 \forall x A 通常被定义为在 FOL 中格式良好，即使 A 没有自由出现 x。那么，当然，\forall x A 等价于 A 以及 \exists x A，这样的量词被称为空的。为了证明任何公式都可以重写为仅包含“nextand”的等效公式，检查以下 \lnot、\lor 和 \forall（带有合适的变量）的定义就足够了——这些定义是 Schönfinkel 的。

\begin{align*} \lnot A & \Leftrightarrow_\textrm{df} A\mid^x A \\ A\lor B & \Leftrightarrow_\textrm{df} (A\mid^yA)\mid^x(B \mid^yB) \\ \forall xAx &\Leftrightarrow_\textrm{df} (Ax\mid^yAx)\mid^x(Ax\mid^yAx) \end{对齐*}

例如，\lnot 的定义可以通过以下等价来证明。 A\Leftrightarrow A\land A, A\land A\Leftrightarrow \exists x(A\land A) （假设 x 在 A 中不自由），因此通过替换，\lnot A\Leftrightarrow \lnot\exists x(A \土地A）。

现在我们举一个具体的例子来说明如何将FOL的公式变成只包含\mid^-的公式，然后如何使用U和组合子消除绑定变量。为了给这个过程带来一些兴奋，我们从 (1)：中的句子开始。

(#1)

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

这句话的直接形式化——在数域的前景上——是（#2）中的公式，（其中‘Nx’代表“x是自然数”，‘Px’代表“x是素数” ”和“Gxy”应理解为“x 大于 y”）。

(#2)

\forall y\存在 x(Ny\supset(Px\land Gxy))

该公式等价于 \forall y(Ny\supset\exists x(Px\land Gxy)) 并进一步等价于 \lnot\exists y\lnot(Ny\supset\exists x(Px\land Gxy))。再过一两步，我们就得到 Ny\mid^y(Px\mid^xGxy)。 （除非括号另有说明，否则表达式被认为分组在左侧。例如，Gxy 是 ((Gx)y) 而不是 G(xy)，这可能是基于 FOL 公式中排列括号的最常见方式所预期的.) 不幸的是，最后一个表达式中 \mid^x 和 \mid^y 都不能被 U 替换。然而，如果 G 的参数被排列，则可以进行前面的约简。组合器之一 \textsf{C} 完全满足了需要：Gxy 可以更改为 \textsf{C}Gyx （请参阅第 2.1 节中组合器的定义）。也就是说，我们有 Ny\mid^y(Px\mid^x\textsf{C}Gyx)，然后是 Ny\mid^yUP (\textsf{C}Gy)。[4]该表达式可能给人的印象是 y 是 UP(\textsf{C}Gy) 的最后一个分量，它是 \mid^y 的第二个参数，但事实并非如此。表达式内的分组不能被忽视，需要另一个组合器 \textsf{B} 将 UP(\textsf{C}Gy) 转换为所需的形式 \textsf{B}(UP)(\textsf{C}G) y。从 Ny\mid^y\textsf{B}(UP)(\textsf{C}G)y，我们再一步得到 UN(\textsf{B}(UP) (\textsf{C}G)) 。这个表达式完全没有变量，并且它也使得 FOL 中绑定变量的重命名变得容易理解：给定前两个元素不同的两个（不同）变量序列，将上述过程反转会产生以下公式： (2)：中公式的字母变体（逻辑上等价）。

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