在一阶逻辑中，我们证明一个理论中的命题通常有两种思路。一种是通过形式演绎的方法直接给出证明，而另一种方法是，根据哥德尔完全性定理，我们可以通过证明满足已知理论的所有模型都满足给定命题来间接的证明该命题。第一种思路是有限主义的，这样的证明是可以在一阶算术中形式化的，因此，我们可以说证明是在一阶算术的框架下进行的；而第二种方法则往往要涉及到无穷，这样的证明往往在二阶算术或者ZFC框架下进行。

      杨森老师首先仔细分析了这两种思路并分别举例说明。然后分析第二种思路，我们发现如果给定的理论本身就是ZFC，这时我们通过第二种方式的证明就变成了“在ZFC框架下证明ZFC可以证明某命题”，为了避免这种奇怪的表述，结合ZFC本身的性质，根据ZFC中的“反射定理”，我们可以找到证明ZFC中命题的第三种思路，也就是使用可数传递模型证明。于是证明就变成了”在ZFC框架下证明可数传递模型可以证明某命题“。接下来杨森老师给出了具体的例子，先简要的介绍了集合论中的力迫法（forcing），然后以力迫法为工具，采用前面提到的第三种思路证明了ZFC中的Silver定理。值得注意的是，在运用力迫法时，杨老师紧密地联系了前面的第二个例子，将力迫法和群论中的代数扩张和伽罗瓦理论作对比，指出了两者的相似性，也让我们加深了对力迫法的理解。整个讲座思路连贯，结构清晰，老师同学们听完后都对使用可数传递模型和力迫法证明ZFC定理有了深刻的认识。

　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　（方楠）