逻辑函数的本质——Schönfinkel论文解读
函数的本质——Schönfinkel论文解读
0. 开场白
断断续续，一直在研读Schönfinkel的那篇划时代论文：《论数理逻辑的基本构件》。原文是德语，我读的是英译本(On the building blocks of mathematical logic)，收录在《From Frege to Gödel: A Source Book in Mathematics, 1879-1931》，译者是Stefan Bauer-Mengelberg。
这篇论文的口头发表的时间是1920年12月7日，场合是哥廷根大学数学学会的年会；书面发表是在近四年后的1924年3月，出版人是Heinrich Behmann。
这篇论文，我前前后后读了4遍，现在正读第5遍，每一遍都有新的体会，第5遍我几乎是字斟句酌，时时停下来思考，同时把论文中的所有推理式都做了一遍。论文不长，难度也不是很大，但就是在这样一篇论文中，一个全新的概念诞生了：函数演算(function calculus)，第一次在逻辑学中引入了计算的概念。毫不夸张地说，这篇论文影响了当时一大批著名的学者，包括Haskell Curry、Alonzo Church、von Neumann、W.V.Quine、Bernays，以及这些学者的学生。包括我们现在熟知的组合子逻辑、λ-演算、递归函数理论，无一不是在这篇论文的影响下产生、发展起来的。
任何人若对逻辑、计算以及逻辑与计算的关系有强烈兴趣，这篇论文是必读之文献，除了其重要性，更多的是，它给你的启迪比现代任何一本关于计算、λ-演算、组合子逻辑的专著都要多；它见证了在20世纪20年代，逻辑学是如何一步步成为现代计算理论的蜕变过程。
这些年看了不少的专著、论文和教科书，但是唯独这篇论文让我难以忘怀，因为我随同作者一同来到了现代可计算函数理论的源头，我和作者在不同的时空背景下重新体验了一个影响了20世纪下半叶直到今天仍然影响我们的伟大理论——可计算函数——计算机的理论模型从蛹化蝶的每一步骤，读到尽兴处甚至击节叫好，忘乎所以。
这篇小文，我希望不但把原作者的思想传达给读者，而且把我自己读论文时的感动之情和读者分享。
1. 时代背景和前提知识
20世纪20年代，离怀特海、罗素那部鸿篇巨著《数学原理》的出版仅仅10年，企图将全部数学理论归结为一阶逻辑的期望似乎已经成真。在这部著作的影响下，希尔伯特德国哥廷根大学发起了希尔伯特计划，试图用公理化的方法和有限的推理手段进一步将全部数学理论统一在一个统一的公理体系之下。这个公理体系的基本精神，就是爱因斯坦所说：从最小数量的假说或公理出发通过逻辑演绎推理说明最大数量的实验事实。当然，数学不是实验科学，通过逻辑演绎推理从给定的公理和已证明的定理得到新的数学定理这是希尔伯特计划的基本目标。按照这个精神，许多学者提出，命题逻辑中的五种运算，否定、合取、析取、蕴含和双蕴含，能否设定其中的一种为未定义运算，然后从这个运算推理、派生其余运算。《数学原理》中的方法是，以否定、蕴含为原生运算，派生其它。而弗雷格则是利用否定和析取。现在以否定和析取为例，从否定和析取到蕴含式的永真式可以派生蕴含，利用德摩根公式可以从否定和析取得到合取，从蕴含合取可以得到双蕴含。其实，五个逻辑运算符，取否定和析取、合取、蕴含中任何一个，都可以派生其余三个。
如果现代公理化的精神就是要减少预设概念和无证明公理的数量，那么，具体到逻辑，能否从更少的逻辑运算派生其余的运算？换句话说，如果从五个连接符中仅仅选择一个作为其基本运算，能否派生其它？经验证明那是完全不可行的。唯一的办法就是为此再加上一个新的连接符，从这个新连接符派生出其它五个逻辑运算。想到这个思路并加以实现的就是美国逻辑学家Henry Sheffer，这个新逻辑连接符通常用“|”表示，所以又称作“Sheffer竖线”。从现代角度看“Sheffer竖线”，其实就是“与非”(nand)的概念：~(p ∧ q)，合取的否定。“与非”的真值表如下：

有了这个新的逻辑运算，其它运算都可以从它派生：
~p = p|p
p ∨ q = (p|p) | (q|q) = ~p | ~q
p ∧ q = (p|q) | (p|q) = ~(p | q)
p → q = p | (q|q) = ~p ∨ q
p ⟷ q = (p | (q|q)) | (q | (p|p)) = (p → q) ∧ (q → p)
为了加深理解，读者最好按照真值表自己确认一下等号两端真值表相等，并且尽快使自己熟悉这个新的逻辑运算。
当年Sheffer发明这个“竖线”逻辑连接符的唯一目的是减少未定义逻辑连接符的数量，因为有了这个连接符，理论上已经不需要其它任何逻辑连接符，符合希尔伯特公理化的一个基本精神：用最少的未定义概念和最少的未证明命题——公理作为数学理论的基础。
显然，Schönfinkel的眼光和洞见比Sheffer又高了一个层次，他从Sheffer的竖线连接符看到了组合的概念——用两个已知运算定义一个新运算，或者说用一个新运算代替两个已知运算——这个新运算就成为两个已知运算的组合运算。如果你读了本系列的其它两篇关于组合子逻辑的笔记，那么你现在就可以意识到这就是组合函数的概念——组合子。现在设三个逻辑连接符为函数，设否定函数为N、合取函数为C，那么就得到
CNpq，把CN抽象化，得到Q
QCN，抽象化的QCN就是竖线函数S
S = QCN
所以，
Sxy = QCNxy
Schönfinkel的眼光独到之处就在于他能够在否定和合取的运算之上抽取出“组合”的概念后用这个组合来定义竖线函数：S = QCN。有了这个概念，Schönfinkel认为，像xy、pq之类的命题、命题函数、变量的概念统统不再需要了，因为这些代表命题、命题函数的变量只不过是函数参数的占位符而已，和命题逻辑的本质——合成句子命题真值的确定没有实质性的关系。30多年后，Curry在《组合子逻辑·第一卷》中重复了这个观点：“显然，逻辑命题并不关心像p、q之类符号以及它们所代表的命题是什么，真正重要的是逻辑运算的关系”。如果你仍然不理解，可以参考本栏目中另一篇笔记《函数的本质——λ演算入门(2)》，其中，我用Lisp语言做了一个简单的命题解释器，其中的所谓“命题”，其实就是一个汉字，而且这些由汉字构成的所谓命题其实都是多余的，其结论和Schönfinkel、Curry完全一致。
在此基础上，Schönfinkel进一步将这个思路扩展到谓词逻辑的量化表达式——带量词的命题句子，并由此提出了“函数演算”的概念。这个概念提出的思路是这样的：
1. 弗雷格首先提出了真值函数的概念，将命题逻辑中逻辑公式的真值看做是由该公式中各个组成部分的真值的函数
2. Schönfinkel将这个思想进一步延伸，将任何命题句都看做真值函数——返回布尔值的函数；
3. Schönfinkel为了用函数作为逻辑的基本元素以代替变量，首次提出：具有固定真值的命题可以看做是常量函数——函数值总一定的函数。例如永真式：例如ƒ(x)=T，无论x的值是什么，函数值永远是T；这时，x可以省略，得：ƒ=T
4. 量化句：有了函数的概念，那么带有量词的命题就可以表示为：
∀xƒ(x)
∃xƒ(x)
5. 将竖线连接符适用于这些命题，建立谓词逻辑的竖线表示法：
∀x~(ƒ(x) ∧ g(x)) =

由于排版的原因，下面的表示法将等同于上述表示法
ƒ(x) |∀x g(x)
其中“|∀x”表示这是个两个命题之间“与非”运算——用竖线连接符表示——相当于ƒ(x)和g(x)合取的全称量化。
而存在量化句等价于
∀xƒ(x) = ~∃~ƒ(x)
因此可以从全称量化句派生存在量化句的与非运算。有了这个基础，下一步我们就可以引入函数演算的概念——function calculus。
6. 在此基础上建立函数演算的体系。逻辑学，在经历了弗雷格、皮亚诺、戴德金、怀特海、罗素之后，在这里开始改道，其核心概念从命题、命题公式、逻辑演算，蜕变为以函数为核心概念的函数演算。
本节的内容相当于论文的第一小节。
【注】原著中量化表达式和现今流行的表示法不同：
全称量化：(x)ƒ(x)
存在量化：(Ex)ƒ(x)
因此在用竖线连接符时，在竖线右上方出现的x就是全称量词，我这里改成了现代通用表示法：|∀x
（待续）
0. 开场白
断断续续，一直在研读Schönfinkel的那篇划时代论文：《论数理逻辑的基本构件》。原文是德语，我读的是英译本(On the building blocks of mathematical logic)，收录在《From Frege to Gödel: A Source Book in Mathematics, 1879-1931》，译者是Stefan Bauer-Mengelberg。
这篇论文的口头发表的时间是1920年12月7日，场合是哥廷根大学数学学会的年会；书面发表是在近四年后的1924年3月，出版人是Heinrich Behmann。
这篇论文，我前前后后读了4遍，现在正读第5遍，每一遍都有新的体会，第5遍我几乎是字斟句酌，时时停下来思考，同时把论文中的所有推理式都做了一遍。论文不长，难度也不是很大，但就是在这样一篇论文中，一个全新的概念诞生了：函数演算(function calculus)，第一次在逻辑学中引入了计算的概念。毫不夸张地说，这篇论文影响了当时一大批著名的学者，包括Haskell Curry、Alonzo Church、von Neumann、W.V.Quine、Bernays，以及这些学者的学生。包括我们现在熟知的组合子逻辑、λ-演算、递归函数理论，无一不是在这篇论文的影响下产生、发展起来的。
任何人若对逻辑、计算以及逻辑与计算的关系有强烈兴趣，这篇论文是必读之文献，除了其重要性，更多的是，它给你的启迪比现代任何一本关于计算、λ-演算、组合子逻辑的专著都要多；它见证了在20世纪20年代，逻辑学是如何一步步成为现代计算理论的蜕变过程。
这些年看了不少的专著、论文和教科书，但是唯独这篇论文让我难以忘怀，因为我随同作者一同来到了现代可计算函数理论的源头，我和作者在不同的时空背景下重新体验了一个影响了20世纪下半叶直到今天仍然影响我们的伟大理论——可计算函数——计算机的理论模型从蛹化蝶的每一步骤，读到尽兴处甚至击节叫好，忘乎所以。
这篇小文，我希望不但把原作者的思想传达给读者，而且把我自己读论文时的感动之情和读者分享。
1. 时代背景和前提知识
20世纪20年代，离怀特海、罗素那部鸿篇巨著《数学原理》的出版仅仅10年，企图将全部数学理论归结为一阶逻辑的期望似乎已经成真。在这部著作的影响下，希尔伯特德国哥廷根大学发起了希尔伯特计划，试图用公理化的方法和有限的推理手段进一步将全部数学理论统一在一个统一的公理体系之下。这个公理体系的基本精神，就是爱因斯坦所说：从最小数量的假说或公理出发通过逻辑演绎推理说明最大数量的实验事实。当然，数学不是实验科学，通过逻辑演绎推理从给定的公理和已证明的定理得到新的数学定理这是希尔伯特计划的基本目标。按照这个精神，许多学者提出，命题逻辑中的五种运算，否定、合取、析取、蕴含和双蕴含，能否设定其中的一种为未定义运算，然后从这个运算推理、派生其余运算。《数学原理》中的方法是，以否定、蕴含为原生运算，派生其它。而弗雷格则是利用否定和析取。现在以否定和析取为例，从否定和析取到蕴含式的永真式可以派生蕴含，利用德摩根公式可以从否定和析取得到合取，从蕴含合取可以得到双蕴含。其实，五个逻辑运算符，取否定和析取、合取、蕴含中任何一个，都可以派生其余三个。
如果现代公理化的精神就是要减少预设概念和无证明公理的数量，那么，具体到逻辑，能否从更少的逻辑运算派生其余的运算？换句话说，如果从五个连接符中仅仅选择一个作为其基本运算，能否派生其它？经验证明那是完全不可行的。唯一的办法就是为此再加上一个新的连接符，从这个新连接符派生出其它五个逻辑运算。想到这个思路并加以实现的就是美国逻辑学家Henry Sheffer，这个新逻辑连接符通常用“|”表示，所以又称作“Sheffer竖线”。从现代角度看“Sheffer竖线”，其实就是“与非”(nand)的概念：~(p ∧ q)，合取的否定。“与非”的真值表如下：

 |
有了这个新的逻辑运算，其它运算都可以从它派生：
~p = p|p
p ∨ q = (p|p) | (q|q) = ~p | ~q
p ∧ q = (p|q) | (p|q) = ~(p | q)
p → q = p | (q|q) = ~p ∨ q
p ⟷ q = (p | (q|q)) | (q | (p|p)) = (p → q) ∧ (q → p)
为了加深理解，读者最好按照真值表自己确认一下等号两端真值表相等，并且尽快使自己熟悉这个新的逻辑运算。
当年Sheffer发明这个“竖线”逻辑连接符的唯一目的是减少未定义逻辑连接符的数量，因为有了这个连接符，理论上已经不需要其它任何逻辑连接符，符合希尔伯特公理化的一个基本精神：用最少的未定义概念和最少的未证明命题——公理作为数学理论的基础。
显然，Schönfinkel的眼光和洞见比Sheffer又高了一个层次，他从Sheffer的竖线连接符看到了组合的概念——用两个已知运算定义一个新运算，或者说用一个新运算代替两个已知运算——这个新运算就成为两个已知运算的组合运算。如果你读了本系列的其它两篇关于组合子逻辑的笔记，那么你现在就可以意识到这就是组合函数的概念——组合子。现在设三个逻辑连接符为函数，设否定函数为N、合取函数为C，那么就得到
CNpq，把CN抽象化，得到Q
QCN，抽象化的QCN就是竖线函数S
S = QCN
所以，
Sxy = QCNxy
Schönfinkel的眼光独到之处就在于他能够在否定和合取的运算之上抽取出“组合”的概念后用这个组合来定义竖线函数：S = QCN。有了这个概念，Schönfinkel认为，像xy、pq之类的命题、命题函数、变量的概念统统不再需要了，因为这些代表命题、命题函数的变量只不过是函数参数的占位符而已，和命题逻辑的本质——合成句子命题真值的确定没有实质性的关系。30多年后，Curry在《组合子逻辑·第一卷》中重复了这个观点：“显然，逻辑命题并不关心像p、q之类符号以及它们所代表的命题是什么，真正重要的是逻辑运算的关系”。如果你仍然不理解，可以参考本栏目中另一篇笔记《函数的本质——λ演算入门(2)》，其中，我用Lisp语言做了一个简单的命题解释器，其中的所谓“命题”，其实就是一个汉字，而且这些由汉字构成的所谓命题其实都是多余的，其结论和Schönfinkel、Curry完全一致。
在此基础上，Schönfinkel进一步将这个思路扩展到谓词逻辑的量化表达式——带量词的命题句子，并由此提出了“函数演算”的概念。这个概念提出的思路是这样的：
1. 弗雷格首先提出了真值函数的概念，将命题逻辑中逻辑公式的真值看做是由该公式中各个组成部分的真值的函数
2. Schönfinkel将这个思想进一步延伸，将任何命题句都看做真值函数——返回布尔值的函数；
3. Schönfinkel为了用函数作为逻辑的基本元素以代替变量，首次提出：具有固定真值的命题可以看做是常量函数——函数值总一定的函数。例如永真式：例如ƒ(x)=T，无论x的值是什么，函数值永远是T；这时，x可以省略，得：ƒ=T
4. 量化句：有了函数的概念，那么带有量词的命题就可以表示为：
∀xƒ(x)
∃xƒ(x)
5. 将竖线连接符适用于这些命题，建立谓词逻辑的竖线表示法：
∀x~(ƒ(x) ∧ g(x)) =

 |
由于排版的原因，下面的表示法将等同于上述表示法
ƒ(x) |∀x g(x)
其中“|∀x”表示这是个两个命题之间“与非”运算——用竖线连接符表示——相当于ƒ(x)和g(x)合取的全称量化。
而存在量化句等价于
∀xƒ(x) = ~∃~ƒ(x)
因此可以从全称量化句派生存在量化句的与非运算。有了这个基础，下一步我们就可以引入函数演算的概念——function calculus。
6. 在此基础上建立函数演算的体系。逻辑学，在经历了弗雷格、皮亚诺、戴德金、怀特海、罗素之后，在这里开始改道，其核心概念从命题、命题公式、逻辑演算，蜕变为以函数为核心概念的函数演算。
本节的内容相当于论文的第一小节。
【注】原著中量化表达式和现今流行的表示法不同：
全称量化：(x)ƒ(x)
存在量化：(Ex)ƒ(x)
因此在用竖线连接符时，在竖线右上方出现的x就是全称量词，我这里改成了现代通用表示法：|∀x
（待续）
> 我来回应