小野寛晰教授首先介绍了证明论的历史，从康托尔的集合论开始，讲述了集合论中Comprehension公理引起的悖论以及如何避 免这种悖论。进而引出了形式主义（Formalism）、直觉主义（Intuitionism）、逻辑主义（Logicism）三种思想。形式主义主要有 两个方面：一是形式化逻辑本身，代表人物有希尔伯特和甘岑，二是形式化数学理论，代表人物有皮亚诺、Zermelo、Fraenkel。之后Ono教授着 重介绍了希尔伯特的形式化证明一致性的观点。第二部分主要介绍了甘岑的矢列演算系统、Cut消去定理，以及与希尔伯特系统的对比。第三部分介绍了从子结构 逻辑的角度去看非经典逻辑。子结构逻辑是非经典逻辑研究中非常活跃的一个研究领域。Ono教授从证明论的角度，结合自己的研究成果以及子结构逻辑的发展历 程，解释了什么是子结构逻辑、子结构逻辑研究的目标是什么，以及子结构逻辑有什么具体特征。最后Ono教授介绍了含有新的逻辑联结词“Fusion”联结 词的系统，进而得出结论：逻辑系统之间的差异主要来源于系统中蕴含定义的差异。

（撰稿人：徐超）