Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Andrea De Domenico, Ali Farjami, Krishna Manoorkar, Alessandra Palmigiano, Mattia Panettiere, Xiaolong Wang

TL;DR

This work advances the semantic and syntactic analysis of input/output logic by embedding normative and permission systems into spd-algebras and their slanted expansions, enabling an infinite class of clopen-analytic modal axioms to be characterized by first-order conditions. Building on unified correspondence, it introduces ALBA-style algorithms (ALBA, FLAT) to compute first-order correspondents and, conversely, inverse procedures (Kracht) to recover modal axioms from FO formulas. The results extend Celani’s duality to a broader environment (spd-algebras, distributive lattices, and inductive Kracht formulas), and they support faithful embeddings of IO-logics into interactive proof systems. Practical impact includes modular modal embeddings, canonicity results, and pathways to implementations and provers within LogiKEy, Isabelle/HOL, and Lean for wide-ranging nonclassical logics beyond classical propositional logic.

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.

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

TL;DR

This work advances the semantic and syntactic analysis of input/output logic by embedding normative and permission systems into spd-algebras and their slanted expansions, enabling an infinite class of clopen-analytic modal axioms to be characterized by first-order conditions. Building on unified correspondence, it introduces ALBA-style algorithms (ALBA, FLAT) to compute first-order correspondents and, conversely, inverse procedures (Kracht) to recover modal axioms from FO formulas. The results extend Celani’s duality to a broader environment (spd-algebras, distributive lattices, and inductive Kracht formulas), and they support faithful embeddings of IO-logics into interactive proof systems. Practical impact includes modular modal embeddings, canonicity results, and pathways to implementations and provers within LogiKEy, Isabelle/HOL, and Lean for wide-ranging nonclassical logics beyond classical propositional logic.

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.

Paper Structure

This paper contains 29 sections, 23 theorems, 35 equations, 2 tables, 5 algorithms.

Table of Contents

  1. Introduction
  2. Structure of the paper
  3. Preliminaries
  4. Canonical extensions of bounded lattices
  5. Subordination and (dual) precontact relations on bounded lattices
  6. Slanted algebras associated with spd-algebras
  7. The LE-logic of spd-algebras
  8. Analytic $\mathcal{L}_{\mathrm{LE}}$-axioms
  9. Correspondence
  10. Step 1 (preprocessing).
  11. Step 2 (first approximation).
  12. Step 3 (compactness).
  13. Step 4 (Ackermann lemma).
  14. Step 5 (flattification).
  15. Step 6 (translation):
  16. ...and 14 more sections

Key Result

Proposition 2.2

(cf. de2024obligations2) For any lattice $A$, all $k_1, k_2\in K(A^\delta)$, $o_1, o_2\in O(A^\delta)$, and $u_1, u_2\in A^\delta$,

Theorems & Definitions (68)

  • Definition 2.1
  • Proposition 2.2
  • Proposition 2.3: cf. de2024obligations2, Proposition 2.7
  • Definition 2.4: de2024obligations2, Footnote 16
  • Definition 2.5
  • Definition 2.6
  • Definition 2.7
  • Lemma 2.8: cf. de2021slanted Lemma 3.5
  • Lemma 2.9: cf. de2024obligations2, Lemma 4.7
  • Example 2.10
  • ...and 58 more