邻域结构：互模拟与基本模型论

邻域结构是用于推理非正规模态逻辑的标准语义工具。所有邻域模型的逻辑称为经典模态逻辑。在余代数术语中，邻域框架是逆变幂集函子与其自身复合（记为2^2）的余代数。我们利用这种余代数建模来推导邻域结构之间的等价概念。2^2-互模拟和行为等价是众所周知的余代数概念，并且它们是不同的，因为2^2不保持弱拉回。我们引入了第三个中间概念，其见证关系称为预余同余（基于推出）。我们给出了2^2-互模拟和预余同余的往返式刻画，证明了在单个余代数上，预余同余捕捉了行为等价，并且在邻域结构之间，预余同余比2^2-互模拟能更好地近似行为等价。我们还引入了邻域模型的模态饱和概念，并研究了其与可定义性和像有限性的关系。我们证明了关于模态饱和邻域模型和像有限邻域模型的Hennessy-Milner定理。我们的主要结果是Van Benthem刻画定理的一个类比，以及经典模态逻辑的Craig插值的一个模型论证明。