最早在逻辑系统中发现形式化计算的人，是Moses Schönfinkel。他在1920年哥廷根Hilbert小组的一次学术交流会上向世人展示了后来被称为组合子的技术。

该技术在第一次路演的时候就完善程度惊人，包括带着逆向语法结构递归的S组合子，包括可以图灵完备的SK组合子，包括关于逻辑组合子的想法和单一的逻辑组合子U的定义，包括后来被用作去除bound variable的bracket abstraction技术，实际上这是完全低估了该技术真正内涵的一种理解。

Schönfinkel是第一个在现代意义上理解最一般的高阶函数泛化的人，象λ那样。他也是Curry化的发明者，虽然Curry反复告诉大家这个技术是Schönfinkel发明的，但是几乎没有人愿意把它写作Schönfinkelization，这大概是名字太长的坏处。实际上λ最初的版本也没有柯里化，是后来引入的。

++++

最早在逻辑学复兴时期提出复活亚里士多德的人，是很少人知道的Paul Hertz。Hertz是物理背景，和今天大家最熟悉的作为频率单位的Hertz有亲戚关系。在1920年代末接近1930年的时候，Hertz也在哥廷根，在「逻辑工厂」的隔壁，他非常熟悉Hilbert，Bernays，Ackermann等人的工作，但是他虽然没有明里站出来反对，却暗中认为Hilbert学派走到了错误的路线上去了。

Hertz的贡献是复活亚里士多德三段论的modus barbara。这是一个有点玩笑意味的名字，因为它特指的三段论形式都是all开头的。比如

所有人都是动物
所有动物都是要死的
所以所有人都是要死的

为什么不叫做modus banana，大概是因为banana的第一个a发音是ə，矮盖斯。

亚里士多德学派和斯多葛学派的逻辑观点的不同，对大众来说是一个很细节的问题。

亚里士多德的形式化是

所有a都是b，所有b都是c，那么所有a都是c。

这在逻辑上称为transitivity。实际上它是捕捉到逻辑的结构的。（没有任何逻辑可以reject自反和传递，即逻辑蕴含一定是预序关系，包括模态，相干，子结构逻辑等非经典逻辑。）

斯多葛学派的形式化是

如果a那么b，a，所以b

这叫做肯定前件（前件指a），modus ponens；

如果a那么b，not b，所以not a

这叫做否定后件（后件指b），modus pollens；

亚里士多德的逻辑很明显，在使用上的局限性很大，它只能从命题到命题，即逻辑不是关于命题的，而是关于「关系」的，这是一个非常纯粹的视角。

斯多葛学派的逻辑观则是，逻辑既是关于关系的，也是关于命题的。而后者对于使用函数视角看待逻辑很重要，不然命题变量和真值都没有立锥之地。

Frege是逻辑学史上排名第二的人物，因为它的概念写作一文开启了逻辑的全新时代，其中最重要的是形式化，其次是引入了量化。Frege的逻辑采纳了斯多葛学派的视角，并进一步把逻辑看作函数，这一观点直接影响了后来的几乎所有逻辑学家，包括Russell，Hilbert都持这一视角。

但Hertz是另类。他更倾向于用modus barbara构建逻辑系统，在图论上理解。实际上Hertz直接影响了König在1934年形式化现代图论的工作，König官方鸣谢了Hertz。

但Hertz画图不是为了搞图论。实际上他是物理类数学背景，专业搞科学哲学的。它把从「理想气体」里抽象出来的「ideal element」科学哲学概念，应用在了逻辑上：即把一个具体的逻辑关系表达式看作一个ideal element，用于简化复杂的多元逻辑关系的细节。

他在图上的表达是，比如abcd之间有复杂的箭头指向关系，但是考虑创建一个e，比如让ab指向e，e再指向cd，这样用一个关系替代原来的多个关系。

基于此，Hertz发明了他独一无二的书写逻辑的方式，一个大横线上面是逻辑关系，下面也是逻辑关系。这是今天对计算机语言理论和现代证明论有了解的人再熟悉不过的东西。是的，他来自Paul Hertz，虽然今天大家把通常它归功给Gerhard Gentzen。事实上Hertz不是顶流的逻辑学家，他主要提供insight。Gentzen的最初的论文几乎完全采用了Hertz的系统，但很快，天才的Gentzen就创世纪般的把系统严格化，提出了可靠且完备的自然演绎与矢列演算，拉开了现代证明论的帷幕。

++++

Schönfinkel因为身体健康原因，把完善整个现代计算系统形式化的机会留给了Church和Curry。Hertz则因为非逻辑专业，把接力棒交给了Gentzen。

但是科学有一个很重要的特点，就是第一个capture一个概念的人，他们的思想之深邃，洞见之深远，后来的集大成者未必能真正超越。

++++

今天能一口气写这么多是因为，基于Schonfinkel和Hertz的原始思想，我找到了

1 证明论里的intro-elim规则对称性的根本原因
2 在类型论和现代计算机语言理论里被捧到信仰和神迹高度的柯里霍华德同构是可证明的，但系统中两个反人类的设定之一，一个奇怪的对称性，需要有良好的解释

其实二者都源于modus barbara的四元形式，对任意两个关系

A⊢B和C⊢D，用矢列的写法，同时应用蕴含左引入和右引入

A⊢B C⊢D
--------------
B⊃C⊢A⊃D

C⊢D A⊢B
--------------
D⊃A⊢C⊃B

注意前提是与（conjunction）关系，对称的，所以结论能整个反向回去。如果把⊢也理解成⊃，结论整个倒回去了，成为序论里的对偶的例子。（当然这不奇怪，蕴含是序）。不过这个对称性要补充一下，这两个前提到结论不是能从结论到前提反向回去的，蕴含右引入可以倒回去因为演绎定理的存在，是等价关系。但是左引入不行，不可逆。而如果先把两个矢列的前件和后件分别混在一起，又没法引入蕴含了。

对于证明论规则，如果其中一个是intro，另一个就是elim。

而把这个对称性和组合子/λ碰撞一下，就能找出柯霍同构的根源。是的不要怀疑，柯霍同构不是什么神迹，是可以rigorously proved，只是系统的设定肥肠反人类，应了爱因斯坦的老话：

如果一个想法第一眼看上去不是愚蠢至极，那么它是没希望的。

几个小时前我盯着一沓纸上的公式终于看出来这个对称性是怎么形成的了。细节就不说了，准备发论文了。