Correspondence and Inverse Correspondence for Input/Output Logic and Region-Based Theories of Space

TL;DR

This paper advances the algebraic and modal semantics of input/output logic by extending characterizations, algorithms, and dualities to infinite classes of conditions, facilitating their implementation in formal systems.

Contribution

It introduces new modal characterizations, algorithms for first-order correspondents, and extends duality results to broader classes of relations in input/output logic.

Findings

Extended modal characterizations for infinite classes of conditions.

Algorithms for computing first-order correspondents and modal axioms.

Extended duality results for subordination, precontact, and dual precontact relations.

Abstract

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.