一句话：系统研究余代数模态逻辑中的析取基概念，建立模拟定理、Lyndon 定理与一致插值等范式与模型论结果。
析取基此前用于余代数 mu-演算的通用完全性证明，本文将其作为余代数模态逻辑范式的通用框架独立研究。作者证明，一步层面存在析取基会带来良好性质，尤其得到模拟定理：交替自动机可转化为等价非确定自动机。据此建立完整不动点逻辑、无不动点片段与一步片段的 Lyndon 定理，并给出完整 mu-演算及其无不动点片段的一致插值。文章还讨论析取基的存在性及其与 Moss 的 nabla 模态的关系，指出 nabla 公式为许多逻辑提供析取基，但分级模态逻辑等情形下析取基仍能给出有用范式；并证明析取基在逻辑的和、积与复合下保持，给出范畴论表述的部分解。
We present the concept of a disjunctive basis as a generic framework for normal forms in modal logic based on coalgebra. Disjunctive bases were defined in previous work on completeness for modal fixpoint logics, where they played a central role in the proof of a generic completeness theorem for coalgebraic mu-calculi. Believing the concept has a much wider significance, here we investigate it more thoroughly in its own right. We show that the presence of a disjunctive basis at the "one-step" level entails a number of good properties for a coalgebraic mu-calculus, in particular, a simulation theorem showing that every alternating automaton can be transformed into an equivalent nondeterministic one. Based on this, we prove a Lyndon theorem for the full fixpoint logic, its fixpoint-free fragment and its one-step fragment, and a Uniform Interpolation result, for both the full mu-calculus and its fixpoint-free fragment. We also raise the questions, when a disjunctive basis exists, and how disjunctive bases are related to Moss' coalgebraic "nabla" modalities. Nabla formulas provide disjunctive bases for many coalgebraic modal logics, but there are cases where disjunctive bases give useful normal forms even when nabla formulas fail to do so, our prime example being graded modal logic. We also show that disjunctive bases are preserved by forming sums, products and compositions of coalgebraic modal logics, providing tools for modular construction of modal logics admitting disjunctive bases. Finally, we consider the problem of giving a category-theoretic formulation of disjunctive bases, and provide a partial solution.Comment: This is a corrected version of the paper arXiv:1710.10706 published originally on 26/3, 2019
@article{paperbot1661,
title = {Disjunctive bases: normal forms and model theory for modal logics},
author = {Sebastian Enqvist and Yde Venema},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 1},
year = {2022},
doi = {10.23638/lmcs-15(1:30)2019}
}