Editing Admissible rule (section)

==Decidability and reduced rules==

The basic question about admissible rules of a given logic is whether the set of all admissible rules is [[decidable set|decidable]]. Note that the problem is nontrivial even if the logic itself (i.e., its set of theorems) is [[decidability (logic)|decidable]]: the definition of admissibility of a rule ''A''/''B'' involves an unbounded [[universal quantifier]] over all propositional substitutions. Hence ''a priori'' we only know that admissibility of rule in a decidable logic is <math>\Pi^0_1</math> (i.e., its complement is [[recursively enumerable]]). For instance, it is known that admissibility in the bimodal logics ''K''<sub>''u''</sub> and ''K''4<sub>''u''</sub> (the extensions of ''K'' or ''K''4 with the [[universal modality]]) is undecidable.<ref>Wolter & Zakharyaschev (2008)</ref> 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 relation|transitive]] modal logics were constructed by [[Vladimir V. Rybakov|Rybakov]], using the '''reduced form of rules'''.<ref>Rybakov (1997), §3.9</ref> A modal rule in variables ''p''<sub>0</sub>, ... , ''p''<sub>''k''</sub> is called reduced if it has the form
:<math>\frac{\bigvee_{i=0}^n\bigl(\bigwedge_{j=0}^k\neg_{i,j}^0p_j\land\bigwedge_{j=0}^k\neg_{i,j}^1\Box p_j\bigr)}{p_0},</math>
where each <math>\neg_{i,j}^u</math> is either blank, or [[logical negation|negation]] <math>\neg</math>. 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 variable]]s 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 <math>\textstyle\bigvee_{i=0}^n\varphi_i/p_0</math> be a reduced rule as above. We identify every conjunction <math>\varphi_i</math> with the set <math>\{\neg_{i,j}^0p_j,\neg_{i,j}^1\Box p_j\mid j\le k\}</math> of its conjuncts. For any subset ''W'' of the set <math>\{\varphi_i\mid i\le n\}</math> of all conjunctions, let us define a [[Kripke model]] <math>M=\langle W,R,{\Vdash}\rangle</math> by
:<math>\varphi_i\Vdash p_j\iff p_j\in\varphi_i,</math>
:<math>\varphi_i\,R\,\varphi_{i'}\iff\forall j\le k\,(\Box p_j\in\varphi_i\Rightarrow\{p_j,\Box p_j\}\subseteq\varphi_{i'}).</math><!-- \mathrel{R} is parsed but deleted by texvc. bloody hell -->
Then the following provides an algorithmic criterion for admissibility in ''K''4:<ref>Rybakov (1997), Thm. 3.9.3</ref>

'''Theorem'''. The rule <math>\textstyle\bigvee_{i=0}^n\varphi_i/p_0</math> is ''not'' admissible in ''K''4 if and only if there exists a set <math>W\subseteq\{\varphi_i\mid i\le n\}</math> such that
#<math>\varphi_i\nVdash p_0</math> for some <math>i\le n,</math>
#<math>\varphi_i\Vdash\varphi_i</math> for every <math>i\le n,</math>
#for every subset ''D'' of ''W'' there exist elements <math>\alpha,\beta\in W</math> such that the equivalences
::<math>\alpha\Vdash\Box p_j</math> if and only if <math>\varphi\Vdash p_j\land\Box p_j</math> for every <math>\varphi\in D</math>
::<math>\alpha\Vdash\Box p_j</math> if and only if <math>\alpha\Vdash p_j</math> and <math>\varphi\Vdash p_j\land\Box p_j</math> for every <math>\varphi\in D</math>
:hold for all ''j''.

Similar criteria can be found for the logics ''S''4, ''GL'', and ''Grz''.<ref>Rybakov (1997), Thms. 3.9.6, 3.9.9, 3.9.12; cf.&nbsp;Chagrov&nbsp;&amp;&nbsp;Zakharyaschev&nbsp;(1997), §16.7</ref> Furthermore, admissibility in intuitionistic logic can be reduced to admissibility in ''Grz'' using the [[modal companion|Gödel–McKinsey–Tarski translation]]:<ref>Rybakov (1997), Thm. 3.2.2</ref>
:<math>A\,|\!\!\!\sim_{IPC}B</math> if and only if <math>T(A)\,|\!\!\!\sim_{Grz}T(B).</math>

Rybakov (1997) developed much more sophisticated techniques for showing decidability of admissibility, which apply to a robust (infinite) class of transitive (i.e., extending ''K''4 or ''IPC'') modal and superintuitionistic logics, including e.g. ''S''4.1, ''S''4.2, ''S''4.3, ''KC'', ''T''<sub>''k''</sub> (as well as the above-mentioned logics ''IPC'', ''K''4, ''S''4, ''GL'', ''Grz'').<ref>Rybakov (1997), §3.5</ref>

Despite being decidable, the admissibility problem has relatively high [[Computational complexity theory|computational complexity]], even in simple logics: admissibility of rules in the basic transitive logics ''IPC'', ''K''4, ''S''4, ''GL'', ''Grz'' is [[NEXP|coNEXP]]-complete.<ref>Jeřábek (2007)</ref> This should be contrasted with the derivability problem (for rules or formulas) in these logics, which is [[PSPACE]]-complete.<ref>Chagrov & Zakharyaschev (1997), §18.5</ref>