集合范畴的模态理论

我们对集合范畴在其自然态射类下的命题模态有效性进行了分类。所得的有效性依赖于态射类、世界的大小以及允许的替换实例。我们的主要技术工具是等式的一阶模态语言的模态与量词消去定理，将公式简化为划分条件的有限布尔组合和精确基数断言。这为集合的主要范畴提供了精确分类，包括有限集合的完全子范畴和无限集合的完全子范畴。特别是，集合范畴中参数化的有限 $n$ 元世界实现了 $\mathrm{Prepartition}_n$；集合范畴与满射范畴中有限 $n$ 元世界在命题层面实现了 $\mathrm{Grz.3J}_n$；而在仅含无限对象的子范畴中，命题有效性坍缩为平凡的模态理论，而函数与满射的公式有效性恰好是 $\mathrm{Grz.2}$。