正实例邻域逻辑
Positive Instantial Neighbourhood logic: Typed Completeness and Admissible-Open Representation
AI总结：
本文提出正实例邻域逻辑（PINL），一种无否定的模态逻辑，通过两种实例模态处理邻域中的世界，并基于持久双边邻域模型证明了其完备性，同时引入代数语义和典范位拓扑表示。
摘要：
实例邻域逻辑是一种用于邻域框架的模态语言，其中的公式可以表达关于给定世界邻域内出现的世界种类的信息。在本文中，我们研究了正实例邻域逻辑的一个无否定版本，该版本具有两种原始实例模态，一种是盒型，一种是菱形型。由于经典否定不可用，这两种模态被独立处理。我们引入了正实例邻域逻辑（PINL）的语言和证明系统，并将其解释在持久双边邻域模型上。然后，我们定义了一种类型化的持久邻域语义，用作辅助的典范语义来控制见证和共见证条件。这产生了真值引理和相应的PINL完备性结果。在代数方面，我们引入了$2$-$\mathrm{DLIO}$s，即配备了两族实例运算的有界分配格，作为PINL的代数语义。我们通过Lindenbaum $2$-$\mathrm{DLIO}$证明了代数可靠性和完备性。最后，我们构造了典范双拓扑PINL空间，并证明了其可容许正开集的代数与Lindenbaum $2$-$\mathrm{DLIO}$同构。因此，本文给出了正实例邻域逻辑的一个典范可容许开表示，为未来的对偶理论迈出了第一步。
英文摘要：
Instantial neighbourhood logic is a modal language for neighbourhood frames in which formulas can express information about the kinds of worlds occurring inside a neighbourhood of a given world. In this paper, we study a positive, negation- and implication-free version of instantial neighbourhood logic with two primitive instantial modalities, one of \(\Box\)-type and one of \(\Diamond\)-type. Since classical negation is not available, the two modalities are treated independently. We introduce the language and proof system of positive instantial neighbourhood logic (PINL) and interpret it over persistent two-sided neighbourhood models. We then define a typed persistent neighbourhood semantics, used as an auxiliary canonical semantics to control witness and co-witness conditions. This yields a truth lemma and a typed completeness theorem for PINL. On the algebraic side, we introduce \(2\)-$\mathrm{DLIO}$s, bounded distributive lattices equipped with two families of instantial operations, as the algebraic semantics of PINL. We prove algebraic soundness and completeness via the Lindenbaum \(2\)-$\mathrm{DLIO}$. Finally, we construct the canonical bitopological PINL-space and show that the algebra of its admissible positive opens is isomorphic to the Lindenbaum \(2\)-$\mathrm{DLIO}$. Thus the paper establishes a canonical admissible-open representation of positive instantial neighbourhood logic, providing a first step toward a future duality theory.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
