#基石
ETCS 理论简介
集合范畴基本理论的公理简介。
【逻辑学】一阶逻辑及其应用
命题逻辑对推理的分析无法满足我们的需求，我们还需要对“所有”这样的词语分析。本文不涉及元定理的证明。…
【逻辑学】模态逻辑及其应用
发展出（命题）模态逻辑的动机来自于，命题逻辑的实质蕴涵并不总是与自然语言的“如果……那么……”完全相符，因为自然语言中还携带了因果、时间、规范、认知、反事实等信息。由于精力有限，本文涉及的内容会远少于对应的课程讲义。…
关于滤子：极限及“最终”模态词诱导
起因是听说 Lean 现在的 mathlib 中实数是依靠滤子定义的（虽然实际搜索了一下发现当前版本还是改为用 Cauchy 序列定义）。…
【逻辑学】经典命题逻辑及其强可靠性、强完全性
这一节主要讨论的是经典命题逻辑（不同于它的均称为“非经典”），重点在于其强完全性的证明。…