The Completeness Problem for Modal Logic

TL;DR

This paper investigates the complexity of the completeness problem in modal logic, establishing its equivalence to validity and proposing a nondeterministic polynomial-time procedure with a PSPACE oracle for testing formula completeness.

Contribution

It introduces the completeness problem for modal logic, analyzes its complexity, and presents a novel nondeterministic procedure with an oracle for determining formula completeness.

Findings

Completeness and validity share the same complexity in modal logic.

Certain formulas are inherently incomplete within the logic.

A nondeterministic polynomial-time procedure with a PSPACE oracle can determine completeness.

Abstract

We introduce the completeness problem for Modal Logic and examine its complexity. For a definition of completeness for formulas, given a formula of a modal logic, the completeness problem asks whether the formula is complete for that logic. We discover that completeness and validity have the same complexity --- with certain exceptions for which there are, in general, no complete formulas. To prove upper bounds, we present a non-deterministic polynomial-time procedure with an oracle from PSPACE that combines tableaux and a test for bisimulation, and determines whether a formula is complete.