本网讯（通讯员陈一源）11月9日和11月16日晚，德国慕尼黑大学Helmut Schwichtenberg教授通过学术志平台做了关于“自然演绎中证明的范式”（Normal of Forms of Proofs in Natural Deduction）的两场线上讲座。第一场的主题是范式的存在性和唯一性（Existence and Uniqueness），第二场的主题是范式的复杂性（Complexity）。两场讲座分别是公司逻辑与哲学系列讲座第28及29讲。讲座由公司程勇教授主持。两场讲座各2小时，学术氛围活跃，来自海内外共450余人次参加了Schwichtenberg教授的讲座。

第一场讲座中，Schwichtenberg教授从极小逻辑（minimal logic）出发，一步步到达主题——自然演绎中证明的范式的存在性和唯一性，讲座的重点在唯一性部分，前面部分都是在为唯一性部分做铺垫。首先，Schwichtenberg教授在第一部分引入了极小逻辑的概念，指出本次讲座的主题是极小逻辑自然演绎的证明范式。何谓极小逻辑?我们通常把语义完备（有效式均可证）的命题逻辑和一阶逻辑称为经典逻辑（classical logic）。现对经典逻辑做减法，如果不允许使用双否消去规则     （），则经典逻辑退化为直觉主义逻辑（intuitionistic logic）；再对直觉主义逻辑做减法，如果不允许使用“矛盾导致一切”规则     （），则直觉主义逻辑退化为极小逻辑。显然直觉主义逻辑比经典逻辑弱，极小逻辑则比前两者都更弱。在经典逻辑中，析取连接词和存在量词可以分别被合取连接词和全称量词加否定连接词定义。但在极小逻辑中却没有这个性质。Schwichtenberg教授保留了极小逻辑中原有的析取连接词和存在量词，又像在经典逻辑中的那样分别用合取连接词和全称量词加否定连接词定义了一个新的二元连接词和量词，取名弱析取（weak disjunction）和弱存在（weak existence）。Schwichtenberg教授又论述了极小逻辑中析取蕴含了弱析取，存在蕴含了弱存在，但反之不然。这就说明了极小逻辑中弱析取与弱存在是名副其实的“弱”，也说明了在经典逻辑中能互相定义的连接词和量词，在极小逻辑中未必能互相定义。

然后，Schwichtenberg教授在讲座的第二和第三部分介绍了Curry-Howard对应和正规化。Schwichtenberg教授引入Curry-Howard对应的主要思想是：把推演树和Lambda项对应起来，而如果Lambda项可以进行     归约，那么转换之后会形成新的更简洁的Lambda项，其对应的推演树和原来Lambda项对应的推演树相比，显得没有那么冗余。推理树之所以有时会显得冗余，是因为推理树中有一些公式，既是某个引入规则的结论，又是某个消去规则的主前提，好似做了无用功。正规化的目的就是去掉推演树中所有这样的公式，而不具有这样的公式的推演也叫正规推演。Schwichtenberg教授接着证明了所有的推演都能转换成正规推演，即所有的推演均可正规化，主要思路是利用     归约总会进行不下去的性质。于是，证明的范式的“存在性”通过正规推演的存在得以体现。

前面提到了所有的推演均可正规化，所有推演都存在正规推演。Schwichtenberg教授在讲座的第四和第五部分讨论了这样的正规推演对任意给定的推演是否是唯一的。Schwichtenberg教授给出了肯定的答案，并给予了证明。证明的思路是我们只需证明对任意给定的推演，不同的正规化路径能得到相同的结果。根据Curry-Howard对应，这个问题可以转价到Lambda转换的终点与转换路径 （       归约等规则使用的先后顺序）无关上。Schwichtenberg教授先证明了几个相关的引理，然后利用这些引理证明了最终的唯一性，由此证明的范式的“唯一性”通过正规推演的唯一性得以体现。最后，Schwichtenberg教授证明了正规推演的一个很重要的性质，子公式性质：即一个正规推演中出现的所有公式，要么是结论的子公式，要么是没有被消掉的前提的子公式；而这个性质是一般推演未必具有的。

第二场讲座是第一场的后续内容，在第一场讲座中，已经引入了正规化思想和正规推演的子公式特征，并且对任意一个推演，尽管它的正规化过程不同，但它的正规化结果，即得到的正规推演是存在且唯一的。那么，对于任意一个可推演的公式，都能很容易地找到一个正规化推演吗？Schwichtenberg教授认为给每个可推演的公式寻找一个正规化推演是一件不现实的事情。Schwichtenberg教授用一个初始常元，一个一元函数符号和一个三元关系符号，给出了有关的两个前提，然后递归地构造了一个公式序列           ，再详细地证明了任何一个从这两个前提到            的正规推演树，它所具有的结点数与            形成的函数关系式，随着     的增加，会远远大于和     有关的任何一个多项式，并且               越大，与多项式的差和商也会越来越大。这就是所谓的复杂性，它让穷尽所有公式的正规推演变得不可行，证明的范式的“复杂性”通过这个例子得以体现。然后，Schwichtenberg教授围绕着线性双层算术（linear two-sorted arithmetic）、序数（ordinals）和算术系统的复杂性问题展开，讨论算术系统中的复杂证明。Schwichtenberg教授介绍了算术理论的序数分析的重要结果，相关定理的证明环环相扣。

在两场讲座的互动环节，Sam Sanders博士介绍了相关的理论背景，包括希尔伯特的证明论，布劳威尔的直觉主义，经典逻辑和直觉主义逻辑的联系，Curry-Howard对应以及强正规化。程勇教授向Schwichtenberg教授提出能否把极小逻辑的这些结论拓展到经典逻辑中去。Schwichtenberg教授指出由于经典逻辑、直觉主义逻辑和极小逻辑的强度不同，有些结论的拓展还是一个新的问题。陈波教授就讲座第一部分根岑转换（gentzen translation）内容的合法性提出疑问，因为这与通常的转换不同；Schwichtenberg教授指出这种转换不是唯一的，是为了引出后面的定理准备的。最后Fernando Ferreira教授评价称Schwichtenberg教授处理序数、算术系统和快速增长函数（fast growing functions）的方式对员工来说是相当优雅的。

至此，Schwichtenberg教授关于“自然演绎中证明的范式”的两场讲座顺利结束。

（编辑：邓莉萍   审稿：刘慧）