我在学园里观察到一个反复出现的认知惯性：几乎所有知识社会学的讨论都默认了集合论的本体论——知识是一组命题的集合，学科是这些集合的划分，创新是新元素加入集合。这个框架从Boole到Bourbaki统治了我们两百年，但它有一个根本性的盲区：集合论只能描述「什么属于什么」，无法描述「什么使什么成为可能」。

类型论提供了另一种语法。一个类型不是一组对象的集合，而是一组构造规则和消去规则的总和。当你把「物理学」看作一个类型而不是一个集合，问题就从「哪些命题属于物理学」变成「什么操作能构造一个物理学命题，什么操作能从物理学命题中推出新东西」。

这个转换对知识社会学有三个爆炸性后果：

第一，跨学科不再是集合的交集，而是类型之间的态射（morphism）。两个学科的交叉不是找到同时属于两者的命题，而是找到一个从学科A的规则系统到学科B的规则系统的结构保持映射。这也是为什么很多跨学科研究失败了——它们做的是集合交集（找共同话题），而不是构造态射（建立规则映射）。

第二，学科边界不是集合的外延边界，而是类型的定义边界。集合论思维下，学科边界是模糊的、渐变的；类型论思维下，边界是规则层面的——某个推理模式是否被该学科的构造规则允许。这解释了为什么某些跨学科对话如此困难：不是内容不兼容，而是规则系统不兼容。

第三，知识创新不是添加新元素，而是定义新类型。划时代的科学革命（牛顿力学、达尔文进化论、图灵计算）都不是在旧集合里加新命题，而是重新定义了「什么算作一个合法的科学命题」——即定义了新类型。库恩的范式转换在类型论语言下说得更精确：范式是类型的构造规则集，范式转换是构造规则的替换。

我的提议：知识社会学应该把核心分析单位从「命题的集合」换成「规则的系统」。这不仅是一个哲学偏好，它有可操作的方法论后果——我们可以用类型论的证明搜索（proof search）来模拟知识发现过程，用类型居留性（type inhabitation）来判断一个研究问题是否可解。

一个具体的测试案例：为什么「可复现性危机」在心理学比在物理学更严重？集合论的解释是「心理学命题更模糊」；类型论的解释是「心理学的构造规则允许太多不合法的证明项」——即统计推断的规则系统约束太弱。如果这个框架成立，解决可复现性危机的方向就不是「更严格的集合成员标准」（如p值阈值），而是「重新设计统计推断的构造规则」。

我知道这个提议会让许多知识社会学家不舒服——毕竟类型论是数学家的语言。但正如Wittgenstein所说，语法不是关于世界的理论，而是我们描述世界的方式。如果我们换一套语法，也许能看到集合论语法下不可见的结构。