Admissible rule


In logic, a rule of inference is admissible in a formal system if the set of theorems of the system does not change when that rule is added to the existing rules of the system. In other words, every formula that can be derived using that rule is already derivable without that rule, so, in a sense, it is redundant. The concept of an admissible rule was introduced by Paul Lorenzen.

Definitions

Admissibility has been systematically studied only in the case of structural rules in propositional non-classical logics, which we will describe next.
Let a set of basic propositional connectives be fixed. Well-formed formulas are built freely using these connectives from a countably infinite set of propositional variables p0, p1,.... A substitution σ is a function from formulas to formulas that commutes with applications of the connectives, i.e.,
for every connective f, and formulas A1,..., An. A Tarski-style consequence relation is a relation between sets of formulas, and formulas, such that
for all formulas A, B, and sets of formulas Γ, Δ. A consequence relation such that
for all substitutions σ is called structural. A structural consequence relation is called a propositional logic. A formula A is a theorem of a logic if.
For example, we identify a superintuitionistic logic L with its standard consequence relation generated by modus ponens and axioms, and we identify a normal modal logic with its global consequence relation generated by modus ponens, necessitation, and the theorems of the logic.
A structural inference rule is given by a pair, usually written as
where Γ = is a finite set of formulas, and B is a formula. An instance of the rule is
for a substitution σ. The rule Γ/B is derivable in, if. It is admissible if for every instance of the rule, σB is a theorem whenever all formulas from σΓ are theorems. In other words, a rule is admissible if it, when added to the logic, does not lead to new theorems. We also write if Γ/B is admissible.
Every derivable rule is admissible, but not vice versa in general. A logic is structurally complete if every admissible rule is derivable, i.e.,.
In logics with a well-behaved conjunction connective, a rule is equivalent to with respect to admissibility and derivability. It is therefore customary to only deal with unary rules A/''B''.

Examples

  • Classical propositional calculus is structurally complete. Indeed, assume that A/''B is a non-derivable rule, and fix an assignment v'' such that v = 1, and v = 0. Define a substitution σ such that for every variable p, σp = if v = 1, and σp = if v = 0. Then σA is a theorem, but σB is not. Thus the rule A/''B is not admissible either.
  • The Kreisel–Putnam rule
  • The rule
  • The rule
  • Löb's rule
  • The Gödel–Dummett logic, and the modal logic Grz''.3 are structurally complete. The product fuzzy logic is also structurally complete.

    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 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 know that admissibility of rule in a decidable logic is . For instance, it is known that admissibility in the bimodal logics K''u and K4u 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 p0,..., pk 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 such that any logic admits r if and only if it admits 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
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:
Rybakov developed much more sophisticated techniques for showing decidability of admissibility, which apply to a robust class of transitive modal and superintuitionistic logics, including e.g. S4.1, S4.2, S4.3, KC, Tk.
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 in these logics, which is PSPACE-complete.

Projectivity and unification

Admissibility in propositional logics is closely related to unification in the equational theory of modal or Heyting algebras. The connection was developed by Ghilardi. In the logical setup, a unifier of a formula A in the language of a logic L is a substitution σ such that σA is a theorem of L. An L-unifier σ is less general than an L-unifier τ, written as σ ≤ τ, if there exists a substitution υ such that
for every variable p. A complete set of unifiers of a formula A is a set S of L-unifiers of A such that every L-unifier of A is less general than some unifier from S. A most general unifier of A is a unifier σ such that is a complete set of unifiers of A. 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.
An important class of formulas that have a most general unifier are the projective formulas: these are formulas A such that there exists a unifier σ of A such that
for every formula B. Note that σ is an MGU of A. 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: 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, we can effectively construct for any formula A its projective approximation Π: a finite set of projective formulas such that
  1. for every
  2. every unifier of A is a unifier of a formula from Π.
It follows that the set of MGUs of elements of Π is a complete set of unifiers of A. Furthermore, if P is a projective formula, then
for any formula B. Thus we obtain the following effective characterization of admissible rules:

Bases of admissible rules

Let L be a logic. A set R of L-admissible rules 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 that includes and R.
Notice that decidability of admissible rules of a decidable logic is equivalent to the existence of recursive 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. 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 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 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.