Editing Admissible rule (section)

==Bases of admissible rules==

Let ''L'' be a logic. A set ''R'' of ''L''-admissible rules is called a '''basis'''<ref>Rybakov (1997), Def. 1.4.13</ref> of admissible rules, if every admissible rule Γ/''B'' can be derived from ''R'' and the derivable rules of ''L'', using substitution, composition, and weakening. In other words, ''R'' is a basis if and only if <math>\phantom{.}\!{|\!\!\!\sim_L}</math> is the smallest structural consequence relation that includes <math>\vdash_L</math> and ''R''.

Notice that decidability of admissible rules of a decidable logic is equivalent to the existence of recursive (or [[recursively enumerable]]) bases: on the one hand, the set of ''all'' admissible rules is a recursive basis if admissibility is decidable. On the other hand, the set of admissible rules is always co-recursively enumerable, and if we further have a recursively enumerable basis, set of admissible rules is also recursively enumerable; hence it is decidable. (In other words, we can decide admissibility of ''A''/''B'' by the following [[algorithm]]: we start in parallel two [[exhaustive search]]es, one for a substitution ''σ'' that unifies ''A'' but not ''B'', and one for a derivation of ''A''/''B'' from ''R'' and <math>\vdash_L</math>. One of the searches has to eventually come up with an answer.) Apart from decidability, explicit bases of admissible rules are useful for some applications, e.g. in [[proof complexity]].<ref>Mints & Kojevnikov (2004)</ref>

For a given logic, we can ask whether it has a recursive or [[finite set|finite]] basis of admissible rules, and to provide an explicit basis. If a logic has no finite basis, it can nevertheless have an '''independent basis''': a basis ''R'' such that no proper subset of ''R'' is a basis.

In general, very little can be said about existence of bases with desirable properties. For example, while [[tabular logic]]s are generally well-behaved, and always finitely axiomatizable, there exist tabular modal logics without a finite or independent basis of rules.<ref>Rybakov (1997), Thm. 4.5.5</ref> Finite bases are relatively rare: even the basic transitive logics ''IPC'', ''K''4, ''S''4, ''GL'', ''Grz'' do not have a finite basis of admissible rules,<ref>Rybakov (1997), §4.2</ref> though they have independent bases.<ref>Jeřábek (2008)</ref>

===Examples of bases===
*The empty set is a basis of ''L''-admissible rules if and only if ''L'' is structurally complete.
*Every extension of the modal logic ''S''4.3 (including, notably, ''S''5) has a finite basis consisting of the single rule<ref>Rybakov (1997), Cor. 4.3.20</ref>
::<math>\frac{\Diamond p\land\Diamond\neg p}\bot.</math>
*{{ill|Albert Visser|lt=Visser|nl}}'s rules
::<math>\frac{\displaystyle\Bigl(\bigwedge_{i=1}^n(p_i\to q_i)\to p_{n+1}\lor p_{n+2}\Bigr)\lor r}{\displaystyle\bigvee_{j=1}^{n+2}\Bigl(\bigwedge_{i=1}^{n}(p_i\to q_i)\to p_j\Bigr)\lor r},\qquad n\ge 1</math>
:are a basis of admissible rules in ''IPC'' or ''KC''.<ref>Iemhoff (2001, 2005), Rozière (1992)</ref>
*The rules
::<math>\frac{\displaystyle\Box\Bigl(\Box q\to\bigvee_{i=1}^n\Box p_i\Bigr)\lor\Box r}{\displaystyle\bigvee_{i=1}^n\Box(q\land\Box q\to p_i)\lor r},\qquad n\ge0</math>
:are a basis of admissible rules of ''GL''.<ref>Jeřábek (2005)</ref> (Note that the empty disjunction is defined as <math>\bot</math>.)
*The rules
::<math>\frac{\displaystyle\Box\Bigl(\Box(q\to\Box q)\to\bigvee_{i=1}^n\Box p_i\Bigr)\lor\Box r}{\displaystyle\bigvee_{i=1}^n\Box(\Box q\to p_i)\lor r},\qquad n\ge0</math>
:are a basis of admissible rules of ''S''4 or ''Grz''.<ref>Jeřábek (2005, 2008)</ref>