$\mu$-代数的完备化

一个 $\mu$-代数是一个一阶理论的模型，该理论是有界格理论的扩展，带有项对 $(f,\mu_{x}.f)$，其中 $\mu_{x}.f$ 被公理化定义为 $f$ 的最小前缀点，其公理为方程或等式蕴含。标准 $\mu$-代数是完备的，意味着其格归约是一个完备格。我们证明任何非平凡的 $\mu$-代数拟簇都包含一个无法嵌入到完备 $\mu$-代数中的 $\mu$-代数。然后我们聚焦于模态 $\mu$-代数，即命题模态 $\mu$-演算的代数模型。我们证明自由模态 $\mu$-代数满足一个条件——令人联想到自由格的 Whitman 条件——它使我们能够证明 (i) 模态算子在自由模态 $\mu$-代数上是伴随，(ii) $\Sigma_{1}$-运算的最小前缀点满足构造性关系 $\mu_{x}.f = \bigvee_{n \geq 0} f^{n}(\bot)$。这些性质蕴含如下陈述：{\em 自由模态 $\mu$-代数的 MacNeille-Dedekind 完备化是一个完备模态 $\mu$-代数，并且此外典范嵌入保持不动点交替层次结构中的类 $Comp(\Sigma_{1},\Pi_{1})$ 的所有运算。}