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-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 the corresponding completeness result of 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 gives a canonical admissible-open representation of positive instantial neighbourhood logic, providing a first step toward a future duality theory.

翻译：实例邻域逻辑是一种用于邻域框架的模态语言，其中公式可以表达关于给定世界邻域内出现的世界种类的信息。本文研究了一种正面、无否定的实例邻域逻辑版本，包含两种原始实例模态：一种为框类型，另一种为菱类型。由于经典否定不可用，这两种模态被独立处理。我们引入了正面实例邻域逻辑（PINL）的语言和证明系统，并将其解释在持久双面邻域模型上。接着，我们定义了一种类型化持久邻域语义，用作辅助规范语义以控制见证和共见证条件。这引出了PINL的真值引理及相应的完备性结果。在代数方面，我们引入了 \(2\)-$\mathrm{DLIO}$（配备了两种实例运算族的有界分配格），作为PINL的代数语义。通过林登鲍姆 \(2\)-$\mathrm{DLIO}$，我们证明了代数的可靠性和完备性。最后，我们构造了典范比特状PINL空间，并证明了其允许正开集的代数与林登鲍姆 \(2\)-$\mathrm{DLIO}$ 同构。因此，本文给出了正面实例邻域逻辑的典范允许开集表示，为未来的对偶理论迈出了第一步。