报告人：陈至诚

题目：一阶逻辑的代入

时间：2021/3/30 15:10-18:00

地点：二教416

摘要：在一阶逻辑中，“代入”是一种基本的公式变形操作（另一种基本变形操作是“易字”）。在一阶逻辑教材、课程中，代入”、“易字”等概念一般不受重视，对它们性质的讨论往往是“游击战式”的——在要用到的时候给出一个够用的版本，八成也不辅以严格的证明。

       常见教材中对“代入”的定义可分为两类：

1. 直截了当地做替换。 

2. 在替换过程中，适当地进行约束变元易字以保证代入自由。 

        本报告将细致讨论这两种思路下“代入”的一般性定义及其重要性质。