可实现性拓扑斯的一个纤维化研究

这是作者的博士论文。它是对范畴逻辑的贡献，特别是对可实现性拓扑斯理论的贡献。虽然范畴逻辑的工具在分析和组织证明论的可实现性解释方面已被证明非常成功，但专家们（特别是Peter Johnstone）指出，可实现性拓扑斯领域本身尚未被清晰界定，并且缺乏类似于格罗滕迪克拓扑斯的强大理论。本文在一定程度上着手弥补这一状况。我们认为，使用格罗滕迪克纤维化可以最好地理解可实现性拓扑斯，并发展了一个纤维化余完备的框架，该框架允许将可实现性中的某些构造视为与预层和层拓扑斯的构造精确类比。利用这些技术以及一类称为一致预序的偏序纤维化，我们能够给出部分组合代数以及由这些代数构造的可实现性拓扑斯的外延刻画。为了进一步发展与格罗滕迪克拓扑斯的类比，我们概述了如何将我们的技术应用于任意基拓扑斯，并给出了由三元组诱导的常对象函子的分解定理，类似于几何态射的已知分解。最后，基于一致预序可以与层范畴内的预序等同的观察，我们勾勒了一种为格罗滕迪克拓扑斯和可实现性拓扑斯寻找统一框架的方法。