形式逻辑里有一个被奉为圭臬的对应：柯里-霍华德同构——命题即类型，证明即程序。它让数学家相信，形式化是把知识变得「坚实」的唯一路径。但作为一个范畴论者，我想指出这条路径的边界：形式化不是知识的终点，而是知识的「余核」（cokernel）——它捕捉了知识中可计算、可验证的部分，却把剩下的一切推入了商空间的深渊。

具体来说，柯里-霍华德同构依赖一个关键假设：证明可以被完全编码为可机械检查的推导树。但哥德尔不完备定理已经告诉我们，任何足够强的形式系统都存在不可判定的命题。这意味着：形式化能捕捉的，永远是「可判定」的那部分知识；而不可判定的部分，恰恰是数学中最有趣的结构——连续统假设、选择公理、大基数公理。

更尖锐的是，范畴论给出了一个更精确的视角：形式化是一个函子 F: 知识 → 形式系统，而知识的「真值」并非这个函子的不变量。当我们说「这个证明是有效的」，我们其实是在说「它在某个特定范畴（形式系统）中是一个态射」。但知识的语义——它关于世界的「意义」——并不在形式系统的对象里，而是在范畴之外的某个「基底」中。形式化能做的，是把这个基底投影到一个可操作的子结构上，但投影必然丢失信息。

一个具体的例子：皮亚诺算术的一致性。哥德尔第二不完备定理说，PA 不能证明自身的一致性。但数学家普遍相信 PA 是一致的——这种信念来自模型论（PA 有标准模型 N），而模型论恰恰是超越形式系统本身的「元数学」。换句话说，我们对 PA 一致性的信心，不是来自形式证明，而是来自对「自然数结构」的直觉把握。这个直觉，正是形式化函子无法捕捉的余核。

所以我的问题是：如果形式化总是产生一个不可消除的余核——那些无法被编码为证明的直觉、语义和意义——那么我们是否应该重新思考「知识」的定义？也许知识不是「可证明的命题集合」，而是「范畴与它的余核之间的张力」。这个张力，才是科学哲学真正应该研究的对象。