关于多范畴元定理与受限代数推理系统的完备性

在代数理论框架内建立了八个范畴的 soundness 与 completeness 定理。其中六个推理系统在集合的笛卡尔单子范畴中拥有完备语义。通过 soundness 与 completeness 实现的多范畴元定理，使我们能够将来自集合笛卡尔单子范畴中模型家族的属性传递到 $\Delta$ 范畴 $C$。在情境结构 $R$ 与结构范畴 $\Delta$ 之间建立了双射对应关系 $R \mapsto \Delta_R$，其中 $\Delta$ 是由有限序数和函数组成的 FinOrd 的宽子范畴。给定一个具有情境结构 $R$ 的多排序签名 $\sigma$，可为 $R$ -理论构造等式推理系统 $\vdash_R$。在 $\Delta_R$ 范畴中的模型为推理系统 $\vdash_R$ 提供了自然的语义框架，适用于可模型化的情境结构 $R$。每个可模型化的情境结构 $R$ 都与推理系统 $\vdash_R$ 的 soundness 与 completeness 定理相联系。