论文标题
在积极逻辑中类型太空函数和解释
Type space functors and interpretations in positive logic
论文作者
论文摘要
我们构造一个2等价$ \ Mathfrak {CohTheory}^\ text {op} \ simeq \ Mathfrak {typespacefunc} $。这里$ \ mathfrak {cohtheory} $是2类正理论，$ \ mathfrak {typespacefunc} $是类型太空函数的2类。我们对正面逻辑的解释进行了精确的定义，这将是$ \ mathfrak {cohtheory} $中的1个细胞。这些两个细胞是可定义的同态。两等价限制在类别的双重性上，确切地说是理论与其类型空间的集合（即其类型太空函数）相同。 在表征那些作为类型太空函子的函子时，我们发现它们是（相干）高do的特定实例。这将两种不同的思想流派与理论的逻辑结构联系起来。 关键成分，deligne的完整定理，源自托普斯理论，在该理论中，积极理论以相干理论的名义进行了研究。
We construct a 2-equivalence $\mathfrak{CohTheory}^\text{op} \simeq \mathfrak{TypeSpaceFunc}$. Here $\mathfrak{CohTheory}$ is the 2-category of positive theories and $\mathfrak{TypeSpaceFunc}$ is the 2-category of type space functors. We give a precise definition of interpretations for positive logic, which will be the 1-cells in $\mathfrak{CohTheory}$. The 2-cells are definable homomorphisms. The 2-equivalence restricts to a duality of categories, making precise the philosophy that a theory is `the same' as the collection of its type spaces (i.e. its type space functor). In characterising those functors that arise as type space functors, we find that they are specific instances of (coherent) hyperdoctrines. This connects two different schools of thought on the logical structure of a theory. The key ingredient, the Deligne completeness theorem, arises from topos theory, where positive theories have been studied under the name of coherent theories.
