Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Decidability of Being a Union-splitting

Tenyo Takahashi

TL;DR

This work resolves the long-standing question of whether the union-splitting property in the lattice $\mathsf{NExt}{\mathsf{K}}$ is decidable by giving a semantic characterization in terms of finite modal algebras and a constructive decision procedure. It shows that such logics are exactly those axiomatizable over $\mathsf{K}$ by Jankov formulas of finite subdirectly irreducible algebras of finite height, enabling enumeration and extraction of finite axiomatizations; it also proves that $\mathsf{KD}$ is the largest union-splitting and that $\mathsf{K}+\top$ is not. As a corollary, the paper establishes the decidability of the axiomatization problem and of (un)decidable formulas for $\mathsf{NExt}{\mathsf{K}}$, linking these decision problems in a novel way and resolving questions from prior surveys.

Abstract

Many logical properties are known to be undecidable for normal modal logics, with few exceptions such as consistency and coincidence with $\mathsf{K}$. This paper shows that the property of being a union-splitting in $\mathsf{NExt}\mathsf{K}$, the lattice of normal modal logics, is decidable, thus answering the open problem [WZ07, Problem 2]. This is done by providing a semantic characterization of union-splittings in terms of finite modal algebras. Moreover, by clarifying the connection to union-splittings, we show that in $\mathsf{NExt}\mathsf{K}$, having a decidable axiomatization problem and being a (un)decidable formula are also decidable. The latter answers [CZ97, Problem 17.3] for $\mathsf{NExt}\mathsf{K}$.

Decidability of Being a Union-splitting

TL;DR

This work resolves the long-standing question of whether the union-splitting property in the lattice is decidable by giving a semantic characterization in terms of finite modal algebras and a constructive decision procedure. It shows that such logics are exactly those axiomatizable over by Jankov formulas of finite subdirectly irreducible algebras of finite height, enabling enumeration and extraction of finite axiomatizations; it also proves that is the largest union-splitting and that is not. As a corollary, the paper establishes the decidability of the axiomatization problem and of (un)decidable formulas for , linking these decision problems in a novel way and resolving questions from prior surveys.

Abstract

Many logical properties are known to be undecidable for normal modal logics, with few exceptions such as consistency and coincidence with . This paper shows that the property of being a union-splitting in , the lattice of normal modal logics, is decidable, thus answering the open problem [WZ07, Problem 2]. This is done by providing a semantic characterization of union-splittings in terms of finite modal algebras. Moreover, by clarifying the connection to union-splittings, we show that in , having a decidable axiomatization problem and being a (un)decidable formula are also decidable. The latter answers [CZ97, Problem 17.3] for .
Paper Structure (4 sections, 19 theorems, 5 equations, 1 figure)

This paper contains 4 sections, 19 theorems, 5 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Decidability of being a union-splitting in $\mathsf{NExt}{\mathsf{K}}$
  4. Axiomatization problems and (un)decidable formulas

Key Result

Theorem 2.1

Let $P$ be a non-trivial property of recursively axiomatizable logics, that is, there are a recursively axiomatizable logic that has $P$ and a recursively axiomatizable logic that does not have $P$. Then it is undecidable whether a recursively axiomatizable logic has $P$.

Figures (1)

  • Figure :

Theorems & Definitions (42)

  • Theorem 2.1: Kuznetsov
  • Definition 2.2
  • Definition 2.3
  • Definition 2.4
  • Definition 2.5
  • Proposition 2.6
  • Theorem 2.7: blok1978degree
  • Theorem 2.8: blok1978degree
  • Corollary 2.9
  • Lemma 3.1
  • ...and 32 more