Teach Myself Logic

这几日主要在研习逻辑学，基本目标是对1940年前数理逻辑的重要成果有一个很好的掌握。

从头梳理了Syntax和Semantics的一些基本定义之后，我首先回顾了一阶逻辑完全性定理的Henkin证明，这一证明我曾学习过多次，但始终自觉理解得不够通彻，在我看来其难度要在同样利用极大一致集的模态命题逻辑完全性的典范模型证明之上——后者我没费太多力气就轻松拿下。这次再看，也只能说是达到了比之前稍好的程度，有机会的话也想学习一下该定理的Hintikka证明和最原始的Godel证明。接着是对模型论至关重要的紧致性定理和Lowenheim-Skolem定理，并特别注意了一下不作为完全性定理的平凡推论，而利用封闭性与膨胀的证明。还有一阶逻辑的不可判定性定理、二阶逻辑的强不完全性定理，这种将判定性问题归约为停机问题并进而给出否定解的方法，我想自己已有了初步的体会。

除了上述这些，我认为需要掌握的“1940年前的重要成果”大致还有Godel不完全性定理以及Tarski真概念不可定义性定理。对这二者的重要性，以及围绕定理本身的字面含义与可能的引申含义的争论，我略知一二，因此是无论如何都希望能将定理面对的问题背景、完整证明以及某种意义上的哲学诠释都理解到精深的程度的。手头的教材上是通过算术的不可判定性定理和不动点定理引出这二者的证明，似乎有些曲折，我阅读起来也感到吃力，计划是结合Enderton以及复旦的教材混合学习，听说后二者给出了严格而有趣的证明。和CS有关的Resolution Theorem以及Logic Programming也想要接触一些，刚好这学期还在修一门程序理论的课程，对PROLOG这种既不面向过程或者对象，也不同于函数式编程的语言很是好奇。

为什么突然开始着手去做这些呢？部分原因可能是受到了一位朋友王轶伦的影响。半年没见，开学第一天我去看望他，听他讲起学年论文的事情，大致是做了有关模态逻辑系统S4下的力迫法的综述，钟盛阳老师看后评价说很有趣，并邀请他去这学期的逻辑学研究生讨论班作报告。对一直颓废的我来说，还真是个不小的震撼。

不过这绝非最主要的原因，毕竟我自以为早就过了因为眼馋别人而跟风做事的阶段。究其根本，当然还是真的想学啊！我很清楚自己对逻辑学的兴趣并没有深到能够将其作为一生的事业，投入到艰深的研究中，一无所成也在所不惜的程度，我也恨极了哲学系普遍存在的那种对学术无知无畏的轻浮态度，所以（从迷梦中醒来后）从不敢以未来的专业人士自居，也断然不会去读相关的学位。只是，对于其中基础性的重大成果，还是好想去了解。康宏逵先生的几篇杂文我读了无数遍，每每读到他与王浩讨论数理逻辑在30-40年代的重大转折，都只恨自己学术不精，不能理解“大数学”集合论如何取代了早期的“大逻辑”，不能理解那些有关形式方法局限性的大成果，更不能理解此后的元数学研究经历了怎样的变化。而当我逐渐接触了这些，每次重读文章时都发现那些技术性内容一点点变得可以理解了之时，也有一种纯粹的幸福。

一年前选修一阶逻辑课程的经历绝对称不上轻松愉快，留下的回忆都是用尽一切可能的时间逐字啃书，对着Overleaf整夜整夜发呆，在一种叫寄存器机的抽象机上写伪汇编程序，用几十行实现一个简单的进位。但穿越了这些之后我也终于有了进一步学习四论的能力。两年前我曾想本科要对四论都有个入门的了解，但那只是无知无畏的表现罢了。现在的想法与其说是那时的延续，不如说是第一次真正产生才对。不是为了获得一个对我近乎羞辱的学位，更不是为了不辜负自己本科生活这种看似严肃实则荒唐的理由，仅仅只是我想去了解，也有了能够了解它们的能力，许多有趣极了的结论就在我已经能看到的地方，有什么理由不去试着攀登呢？