Admissible Rule - Decidability and Reduced Rules

Decidability and Reduced Rules

The basic question about admissible rules of a given logic is whether the set of all admissible rules is decidable. Note that the problem is nontrivial even if the logic itself (i.e., its set of theorems) is decidable: the definition of admissibility of a rule A/B involves an unbounded universal quantifier over all propositional substitutions, hence a priori we only now that admissibility of rule in a decidable logic is (i.e., its complement is recursively enumerable). For instance, it is known that admissibility in the bimodal logics K_u and K4_u (the extensions of K or K4 with the universal modality) is undecidable. Remarkably, decidability of admissibility in the basic modal logic K is a major open problem.

Nevertheless, admissibility of rules is known to be decidable in many modal and superintuitionistic logics. The first decision procedures for admissible rules in basic transitive modal logics were constructed by Rybakov, using the reduced form of rules. A modal rule in variables p₀, …, p_k is called reduced if it has the form

where each is either blank, or negation . For each rule r, we can effectively construct a reduced rule s (called the reduced form of r) such that any logic admits (or derives) r if and only if it admits (or derives) s, by introducing extension variables for all subformulas in A, and expressing the result in the full disjunctive normal form. It is thus sufficient to construct a decision algorithm for admissibility of reduced rules.

Let be a reduced rule as above. We identify every conjunction with the set of its conjuncts. For any subset W of the set of all conjunctions, let us define a Kripke model by

Then the following provides an algorithmic criterion for admissibility in K4:

Theorem. The rule is not admissible in K4 if and only if there exists a set such that

1. for some
2. for every
3. for every subset D of W there exist elements such that the equivalences

if and only if for every

if and only if and for every

hold for all j.

Similar criteria can be found for the logics S4, GL, and Grz. Furthermore, admissibility in intuitionistic logic can be reduced to admissibility in Grz using the Gödel–McKinsey–Tarski translation:

if and only if

Rybakov (1997) developed much more sophisticated techniques for showing decidability of admissibility, which apply to a robust (infinite) class of transitive (i.e., extending K4 or IPC) modal and superintuitionistic logics, including e.g. S4.1, S4.2, S4.3, KC, T_k (as well as the above mentioned logics IPC, K4, S4, GL, Grz).

Despite being decidable, the admissibility problem has relatively high computational complexity, even in simple logics: admissibility of rules in the basic transitive logics IPC, K4, S4, GL, Grz is coNEXP-complete. This should be contrasted with the derivability problem (for rules or formulas) in these logics, which is PSPACE-complete.