We further develop the algebraic approach to input/output logic initiated in \cite{wollic22}, where subordination algebras and a family of their generalizations were proposed as a semantic environment of various input/output logics. In particular: we extend the modal characterizations of a finite number of well known conditions on normative and permission systems, as well as on subordination, precontact, and dual precontact algebras developed in \cite{de2024obligations}, to those corresponding to the infinite class of {\em clopen-analytic inequalities} in a modal language consisting both of positive and of negative unary modal operators; we characterize the syntactic shape of first-order conditions on algebras endowed with subordination, precontact, and dual precontact relations which guarantees these conditions to be the first-order correspondents of axioms in the modal language above; we introduce algorithms for computing the first-order correspondents of modal axioms on algebras endowed with subordination, precontact, and dual precontact relations, and conversely, for computing the modal axioms of which the conditions satisfying the suitable syntactic shape are the first-order correspondents; finally, we extend Celani's dual characterization results between subordination lattices and subordination spaces to a wider environment which also encompasses precontact and dual precontact relations, and relative to an infinite class of first order conditions relating subordination, precontact and dual precontact relations on distributive lattices. The modal characterizations established in the present paper pave the way to establishing faithful embeddings for infinite classes of input/output logics, and hence to their implementation in LogiKEy, Isabelle/HOL, Lean, or other interactive systems.

翻译：我们进一步发展了始于\cite{wollic22}的输入/输出逻辑代数方法，其中从属代数及其一系列推广被提出作为各种输入/输出逻辑的语义环境。具体而言：我们将\cite{de2024obligations}中针对有限数量关于规范与许可系统以及关于从属、预接触和对偶预接触代数的已知条件的模态刻画，扩展到对应于由正负一元模态算子组成的模态语言中无限类{\em 闭开解析不等式}的那些条件；我们刻画了赋予从属、预接触和对偶预接触关系的代数上的一阶条件的句法形态，这些条件保证了它们成为上述模态语言中公理的一阶对应式；我们引入了计算赋予从属、预接触和对偶预接触关系的代数上模态公理的一阶对应式的算法，反之，也引入了计算满足适当句法形态的条件所对应模态公理的算法；最后，我们将Celani关于从属格与从属空间之间的对偶刻画结果扩展到一个更广泛的环境，该环境也包含预接触和对偶预接触关系，并且涉及在分配格上关联从属、预接触和对偶预接触关系的无限类一阶条件。本文建立的模态刻画为建立无限类输入/输出逻辑的忠实嵌入铺平了道路，从而为它们在LogiKEy、Isabelle/HOL、Lean或其他交互式系统中的实现奠定了基础。