#基石

阅读 Trebor 的高观点小册子《类型论简史》的笔记（跳过了范畴语义部分）。…

ETCS 是 Lawvere 的集合范畴基本理论（Elementary Theory of the Category of Sets）。 对此会有一个误解是认为其基本动机是用范畴论来取代集合理论，其实不然，它就是集合论。这些公理是受范畴启发的，并不依赖于拥有一个一般的范畴的定义。…

命题逻辑对推理的分析无法满足我们的需求，我们还需要对“所有”这样的词语分析，因而有了一阶逻辑，在满足一定条件下它是表达能力最强的逻辑系统，但也有其边界。…

发展出（命题）模态逻辑的动机来自于，命题逻辑的实质蕴涵并不总是与自然语言的“如果……那么……”完全相符，因为自然语言中还携带了因果、时间、规范、认知、反事实等信息。由于精力有限，本文涉及的内容会远少于对应的课程讲义。…

起因是听说 Lean 现在的 mathlib 中实数是依靠滤子定义的（但实际搜索了一下发现当前版本还是改为用 Cauchy 序列定义）。…

这一节主要讨论的是经典命题逻辑（不同于它的均称为“非经典”），重点在于其强完全性的证明。…

选了哲学系开的Ⅲ类通识课“逻辑导论”。此文主要是做习题（之后大概也会如此），因此先快速掠过定义：…

发现到时候不一定要读数院的研，考虑可以做逻辑学或者是 AI for math. 仔细阅读本书 Homotopy Type Theory: Univalent Foundations of Mathematics. 这是上学期计概老师推荐的，但当时看得太粗略了。本文包含该书第一章内容。…

本文讨论 Alonzo Church 发明的无类型 λ 演算（λ-calculus）。这是一个类型论与计算理论的基础模型。…