Admissibility has been systematically studied only in the case of structural (i.e. substitution-closed) rules in propositional non-classical logics, which we will describe next.
generated by modus ponens and axioms, and we identify a normal modal logic with its global consequence relation
generated by modus ponens, necessitation, and (as axioms) the theorems of the logic.
[3] In other words, a rule is admissible if it, when added to the logic, does not lead to new theorems.
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.
For instance, it is known that admissibility in the bimodal logics Ku and K4u (the extensions of K or K4 with the universal modality) is undecidable.
[11] Remarkably, decidability of admissibility in the basic modal logic K is a major open problem.
[12] A modal rule in variables p0, ... , pk is called reduced if it has the form where each
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.
[14] Furthermore, admissibility in intuitionistic logic can be reduced to admissibility in Grz using the Gödel–McKinsey–Tarski translation:[15] 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, Tk (as well as the above-mentioned logics IPC, K4, S4, GL, Grz).
[16] 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.
[17] This should be contrasted with the derivability problem (for rules or formulas) in these logics, which is PSPACE-complete.
[18] Admissibility in propositional logics is closely related to unification in the equational theory of modal or Heyting algebras.
It follows that if S is a complete set of unifiers of A, then a rule A/B is L-admissible if and only if every σ in S is an L-unifier of B.
Thus we can characterize admissible rules if we can find well-behaved complete sets of unifiers.
In transitive modal and superintuitionistic logics with the finite model property, one can characterize projective formulas semantically as those whose set of finite L-models has the extension property:[19] if M is a finite Kripke L-model with a root r whose cluster is a singleton, and the formula A holds at all points of M except for r, then we can change the valuation of variables in r so as to make A true at r as well.
Moreover, the proof provides an explicit construction of an MGU for a given projective formula A.
In the basic transitive logics IPC, K4, S4, GL, Grz (and more generally in any transitive logic with the finite model property whose set of finite frame satisfies another kind of extension property), we can effectively construct for any formula A its projective approximation Π(A):[20] a finite set of projective formulas such that It follows that the set of MGUs of elements of Π(A) is a complete set of unifiers of A.
(In other words, we can decide admissibility of A/B by the following algorithm: we start in parallel two exhaustive searches, one for a substitution σ that unifies A but not B, and one for a derivation of A/B from R and
Apart from decidability, explicit bases of admissible rules are useful for some applications, e.g. in proof complexity.
For example, while tabular logics are generally well-behaved, and always finitely axiomatizable, there exist tabular modal logics without a finite or independent basis of rules.
[24] Finite bases are relatively rare: even the basic transitive logics IPC, K4, S4, GL, Grz do not have a finite basis of admissible rules,[25] though they have independent bases.
Hence admissible rules in basic transitive logics do not enjoy the finite model property.
While a general classification of structurally complete logics is not an easy task, we have a good understanding of some special cases.
Intuitionistic logic itself is not structurally complete, but its fragments may behave differently.
[32] On the other hand, the Mints rule is admissible in intuitionistic logic but not derivable, and contains only implications and disjunctions.
The rule is L-admissible if every L-unifier σ of A such that σsi = si for each i is also a unifier of B.
[34] A multiple-conclusion rule is a pair (Γ,Δ) of two finite sets of formulas, written as Such a rule is admissible if every unifier of Γ is also a unifier of some formula from Δ.
For example, one can rephrase the cut-elimination theorem as saying that the cut-free sequent calculus admits the cut rule (By abuse of language, it is also sometimes said that the (full) sequent calculus admits cut, meaning its cut-free version does.)