一阶逻辑对偶
First-Order Logical Duality
摘要：
从逻辑的角度来看，斯通对偶布尔代数涉及理论在经典命题逻辑和他们的收集模型。理论可以被看作是布尔代数的表示，模型的集合可以被拓扑化，这样理论就可以从它的模型空间中恢复出来。这种情况可以被看作是一种形式上的二元性，它把句法和语义两个范畴联系起来，通过归巢中介成一个共同的二元对象，在这种情况下是2。在目前的工作中，我们推广整个安排从命题的一阶逻辑。用一阶逻辑中的布尔范畴代替布尔代数，用模型的拓扑群胚及其同构代替模型空间。由此产生的句法和语义范畴之间的对偶，首先以逆变附加词的形式表达，通过归巢到一个共同的对偶对象（现在是$\Sets$）中来建立，它一度被视为布尔范畴，一度被视为配备有内在拓扑的广群。我们的研究的总体框架是由拓扑斯理论提供的。直接证明的主要结果，但专家将认识到拓扑思想的背景。事实上，语法和语义之间的对偶性实际上是代数和几何之间的对偶性在隐藏在我们形式理论后面的几何态射的两个方向上的表现。在此过程中，我们通过一个简化的相干拓扑覆盖定理，从一个可判定的相干理论的模型广群中构造了它的分类拓扑。
英文摘要：
From a logical point of view, Stone duality for Boolean algebras relates theories in classical propositional logic and their collections of models. The theories can be seen as presentations of Boolean algebras, and the collections of models can be topologized in such a way that the theory can be recovered from its space of models. The situation can be cast as a formal duality relating two categories of syntax and semantics, mediated by homming into a common dualizing object, in this case 2. In the present work, we generalize the entire arrangement from propositional to first-order logic. Boolean algebras are replaced by Boolean categories presented by theories in first-order logic, and spaces of models are replaced by topological groupoids of models and their isomorphisms. A duality between the resulting categories of syntax and semantics, expressed first in the form of a contravariant adjunction, is established by homming into a common dualizing object, now $\Sets$, regarded once as a boolean category, and once as a groupoid equipped with an intrinsic topology. The overall framework of our investigation is provided by topos theory. Direct proofs of the main results are given, but the specialist will recognize toposophical ideas in the background. Indeed, the duality between syntax and semantics is really a manifestation of that between algebra and geometry in the two directions of the geometric morphisms that lurk behind our formal theory. Along the way, we construct the classifying topos of a decidable coherent theory out of its groupoid of models via a simplified covering theorem for coherent toposes.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
