Admissible Rule - Bases of Admissible Rules

Bases of Admissible Rules

Let L be a logic. A set R of L-admissible rule is called a basis 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 is the smallest structural consequence relation which includes 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 rule is a recursive basis if admissibility is decidable. On the other hand, the set of admissible rules is always co-r.e., and if we further have an r.e. basis, it is also r.e., hence it is decidable. (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 σ which unifies A but not B, and one for a derivation of A/B from R and . 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.

For a given logic, we can ask whether it has a recursive or finite basis of admissible rules, and to provide an explicit basis. If a logic has no finite basis, it can nevertheless has 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 logics are generally well-behaved, and always finitely axiomatizable, there exist tabular modal logics without a finite or independent basis of rules. Finite bases are relatively rare: even the basic transitive logics IPC, K4, S4, GL, Grz do not have a finite basis of admissible rules, though they have independent bases.