3.17 第三节课

数学的一致性 推理的有效性vs命题的真 对$F\rightarrow T$为$T$的解释： 真空真理（vacuous truth），错误的前提不限制结论的真假

3.24 第四节课

lean4在未来大有可为，其余领域也需要类似的系统化语言，以便ai使用 wff的结构递归的定义