Admissible rule

This article is about rules of inference in logic systems. For the concept in decision theory, see admissible decision 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 (1955).

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 (for instance, \{\to,\land,\lor,\bot\} in the case of superintuitionistic logics, or \{\to,\bot,\Box\} in the case of monomodal logics). Well-formed formulas are built freely using these connectives from a countably infinite set of propositional variables pn. A substitution σ is a function from formulas to formulas which commutes with the connectives, i.e.,

\sigma f(A_1,\dots,A_n)=f(\sigma A_1,\dots,\sigma A_n)

for every connective f, and formulas A1, …, An. (We may also apply substitutions to sets Γ of formulas, making σΓ = {σA: A Γ}.) A Tarski-style consequence relation[1] is a relation \vdash between sets of formulas, and formulas, such that

  1. A\vdash A,
  2. if \Gamma\vdash A then \Gamma,\Delta\vdash A,
  3. if \Gamma\vdash A and \Delta,A\vdash B then \Gamma,\Delta\vdash B,

for all formulas A, B, and sets of formulas Γ, Δ. A consequence relation such that

  1. if \Gamma\vdash A then \sigma\Gamma\vdash\sigma A

for all substitutions σ is called structural. (Note that the term "structural" as used here and below is unrelated to the notion of structural rules in sequent calculi.) A structural consequence relation is called a propositional logic. A formula A is a theorem of a logic \vdash if \varnothing\vdash A.

For example, we identify a superintuitionistic logic L with its standard consequence relation \vdash_L axiomatizable by modus ponens and axioms, and we identify a normal modal logic with its global consequence relation \vdash_L axiomatized by modus ponens, necessitation, and axioms.

A structural inference rule[2] (or just rule for short) is given by a pair (Γ,B), usually written as

\frac{A_1,\dots,A_n}B\qquad\text{or}\qquad A_1,\dots,A_n/B,

where Γ = {A1, …, An} is a finite set of formulas, and B is a formula. An instance of the rule is

\sigma A_1,\dots,\sigma A_n/\sigma B

for a substitution σ. The rule Γ/B is derivable in \vdash, if \Gamma\vdash B. It is admissible if for every instance of the rule, σB is a theorem whenever all formulas from σΓ are theorems.[3] In other words, a rule is admissible if, when added to the logic, does not lead to new theorems.[4] We also write \Gamma\,|\!\!\!\sim B if Γ/B is admissible. (Note that |\!\!\!\sim is a structural consequence relation on its own.)

Every derivable rule is admissible, but not vice versa in general. A logic is structurally complete if every admissible rule is derivable, i.e., {\vdash}={\,|\!\!\!\sim}.[5]

In logics with a well-behaved conjunction connective (such as superintuitionistic or modal logics), a rule A_1,\dots,A_n/B is equivalent to A_1\land\dots\land A_n/B with respect to admissibility and derivability. It is therefore customary to only deal with unary rules A/B.

Examples

(\mathit{KPR})\qquad\frac{\neg p\to q\lor r}{(\neg p\to q)\lor(\neg p\to r)}
is admissible in the intuitionistic propositional calculus (IPC). In fact, it is admissible in every superintuitionistic logic.[7] On the other hand, the formula
(\neg p\to q\lor r)\to ((\neg p\to q)\lor(\neg p\to r))
is not an intuitionistic tautology, hence KPR is not derivable in IPC. In particular, IPC is not structurally complete.
\frac{\Box p}p
is admissible in many modal logics, such as K, D, K4, S4, GL (see this table for names of modal logics). It is derivable in S4, but it is not derivable in K, D, K4, or GL.
\frac{\Diamond p\land\Diamond\neg p}\bot
is admissible in every normal modal logic.[8] It is derivable in GL and S4.1, but it is not derivable in K, D, K4, S4, S5.
(\mathit{LR})\qquad\frac{\Box p\to p}p
is admissible (but not derivable) in the basic modal logic K, and it is derivable in GL. However, LR is not admissible in K4. In particular, it is not true in general that a rule admissible in a logic L must be admissible in its extensions.

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 (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, hence a priori we only know that admissibility of rule in a decidable logic is \Pi^0_1 (i.e., its complement is recursively enumerable). 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.

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.[12] A modal rule in variables p0, …, pk is called reduced if it has the form

\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},

where each \neg_{i,j}^u is either blank, or negation \neg. 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.

Let \textstyle\bigvee_{i=0}^n\varphi_i/p_0 be a reduced rule as above. We identify every conjunction \varphi_i with the set \{\neg_{i,j}^0p_j,\neg_{i,j}^1\Box p_j\mid j\le k\} of its conjuncts. For any subset W of the set \{\varphi_i\mid i\le n\} of all conjunctions, let us define a Kripke model M=\langle W,R,{\Vdash}\rangle by

\varphi_i\Vdash p_j\iff p_j\in\varphi_i,
\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'}).

Then the following provides an algorithmic criterion for admissibility in K4:[13]

Theorem. The rule \textstyle\bigvee_{i=0}^n\varphi_i/p_0 is not admissible in K4 if and only if there exists a set W\subseteq\{\varphi_i\mid i\le n\} such that

  1. \varphi_i\nVdash p_0 for some i\le n,
  2. \varphi_i\Vdash\varphi_i for every i\le n,
  3. for every subset D of W there exist elements \alpha,\beta\in W such that the equivalences
\alpha\Vdash\Box p_j if and only if \varphi\Vdash p_j\land\Box p_j for every \varphi\in D
\alpha\Vdash\Box p_j if and only if \alpha\Vdash p_j and \varphi\Vdash p_j\land\Box p_j for every \varphi\in D
hold for all j.

Similar criteria can be found for the logics S4, GL, and Grz.[14] Furthermore, admissibility in intuitionistic logic can be reduced to admissibility in Grz using the Gödel–McKinsey–Tarski translation:[15]

A\,|\!\!\!\sim_{IPC}B if and only if T(A)\,|\!\!\!\sim_{Grz}T(B).

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]

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 (1999, 2000). In the logical setup, a unifier of a formula A in a logic L (an L-unifier for short) is a substitution σ such that σA is a theorem of L. (Using this notion, we can rephrase admissibility of a rule A/B in L as "every L-unifier of A is an L-unifier of B".) An L-unifier σ is less general than an L-unifier τ, written as σ ≤ τ, if there exists a substitution υ such that

\vdash_L\sigma p\leftrightarrow \upsilon\tau p

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 (mgu) 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 which have a most general unifier are the projective formulas: these are formulas A such that there exists a unifier σ of A such that

A\vdash_L B\leftrightarrow\sigma B

for every formula B. Note that σ is a mgu of A. In transitive modal and superintuitionistic logics with the finite model property (fmp), 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 in all points of M except for r, then we can change the valuation of variables in r so as to make A true in r as well. Moreover, the proof provides an explicit construction of a 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 fmp 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

  1. P\vdash_L A for every P\in\Pi(A),
  2. every unifier of A is a unifier of a formula from Π(A).

It follows that the set of mgus of elements of Π(A) is a complete set of unifiers of A. Furthermore, if P is a projective formula, then

P\,|\!\!\!\sim_L B if and only if P\vdash_L B

for any formula B. Thus we obtain the following effective characterization of admissible rules:[21]

A\,|\!\!\!\sim_L B if and only if \forall P\in\Pi(A)\,(P\vdash_L B).

Bases of admissible rules

Let L be a logic. A set R of L-admissible rule is called a basis[22] 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 |\!\!\!\sim_L is the smallest structural consequence relation which includes \vdash_L 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 \vdash_L. 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.[23]

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.[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.[26]

Examples of bases

\frac{\Diamond p\land\Diamond\neg p}\bot.
\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
are a basis of admissible rules in IPC or KC.[28]
\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
are a basis of admissible rules of GL.[29] (Note that the empty disjunction is defined as \bot.)
\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
are a basis of admissible rules of S4 or Grz.[30]

Semantics for admissible rules

A rule Γ/B is valid in a modal or intuitionistic Kripke frame F=\langle W,R\rangle, if the following is true for every valuation \Vdash in F:

if \forall x\in W\,(x\Vdash A) for all A\in\Gamma, then \forall x\in W\,(x\Vdash B).

(The definition readily generalizes to general frames, if needed.)

Let X be a subset of W, and t a point in W. We say that t is

We say that a frame F has reflexive (irreflexive) tight predecessors, if for every finite subset X of W, there exists a reflexive (irreflexive) tight predecessor of X in W.

We have:[31]

Note that apart from a few trivial cases, frames with tight predecessors must be infinite, hence admissible rules in basic transitive logics do not enjoy the finite model property.

Structural completeness

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. Namely, any disjunction-free rule or implication-free rule admissible in a superintuitionistic logic is derivable.[32] On the other hand, the Mints rule

\frac{(p\to q)\to p\lor r}{((p\to q)\to p)\lor((p\to q)\to r)}

is admissible in intuitionistic logic but not derivable, and contains only implications and disjunctions.

We know the maximal structurally incomplete transitive logics. A logic is called hereditarily structurally complete, if every its extension is structurally complete. For example, classical logic, as well as the logics LC and Grz.3 mentioned above, are hereditarily structurally complete. A complete description of hereditarily structurally complete superintuitionistic and transitive modal logics was given by Citkin and Rybakov. Namely, a superintuitionistic logic is hereditarily structurally complete if and only if it is not valid in any of the five Kripke frames[9]

Similarly, an extension of K4 is hereditarily structurally complete if and only if it is not valid in any of certain twenty Kripke frames (including the five intuitionistic frames above).[9]

There exist structurally complete logics that are not hereditarily structurally complete: for example, Medvedev's logic is structurally complete,[33] but it is included in the structurally incomplete logic KC.

Variants

A rule with parameters is a rule of the form

\frac{A(p_1,\dots,p_n,s_1,\dots,s_k)}{B(p_1,\dots,p_n,s_1,\dots,s_k)},

whose variables are divided into the "regular" variables pi, and the parameters si. The rule is L-admissible if every L-unifier σ of A such that σsi = si for each i is also a unifier of B. The basic decidability results for admissible rules also carry to rules with parameters.[34]

A multiple-conclusion rule is a pair (Γ,Δ) of two finite sets of formulas, written as

\frac{A_1,\dots,A_n}{B_1,\dots,B_m}\qquad\text{or}\qquad A_1,\dots,A_n/B_1,\dots,B_m.

Such a rule is admissible if every unifier of Γ is also a unifier of some formula from Δ.[35] For example, a logic L is consistent iff it admits the rule

\frac{\;\bot\;}{},

and a superintuitionistic logic has the disjunction property iff it admits the rule

\frac{p\lor q}{p,q}.

Again, basic results on admissible rules generalize smoothly to multiple-conclusion rules.[36] In logics with a variant of the disjunction property, the multiple-conclusion rules have the same expressive power as single-conclusion rules: for example, in S4 the rule above is equivalent to

\frac{A_1,\dots,A_n}{\Box B_1\lor\dots\lor\Box B_m}.

Nevertheless, multiple-conclusion rules can often be employed to simplify arguments.

In proof theory, admissibility is often considered in the context of sequent calculi, where the basic objects are sequents rather than formulas. For example, one can rephrase the cut-elimination theorem as saying that the cut-free sequent calculus admits the cut rule

\frac{\Gamma\vdash A,\Delta\qquad\Pi,A\vdash\Lambda}{\Gamma,\Pi\vdash\Delta,\Lambda}.

(By abuse of language, it is also sometimes said that the (full) sequent calculus admits cut, meaning its cut-free version does.) However, admissibility in sequent calculi is usually only a notational variant for admissibility in the corresponding logic: any complete calculus for (say) intuitionistic logic admits a sequent rule if and only if IPC admits the formula rule which we obtain by translating each sequent \Gamma\vdash\Delta to its characteristic formula \bigwedge\Gamma\to\bigvee\Delta.

Notes

  1. Blok & Pigozzi (1989), Kracht (2007)
  2. Rybakov (1997), Def. 1.1.3
  3. Rybakov (1997), Def. 1.7.2
  4. From de Jongh’s theorem to intuitionistic logic of proofs
  5. Rybakov (1997), Def. 1.7.7
  6. Chagrov & Zakharyaschev (1997), Thm. 1.25
  7. Prucnal (1979), cf. Iemhoff (2006)
  8. Rybakov (1997), p. 439
  9. 1 2 3 Rybakov (1997), Thms. 5.4.4, 5.4.8
  10. Cintula & Metcalfe (2009)
  11. Wolter & Zakharyaschev (2008)
  12. Rybakov (1997), §3.9
  13. Rybakov (1997), Thm. 3.9.3
  14. Rybakov (1997), Thms. 3.9.6, 3.9.9, 3.9.12; cf. Chagrov & Zakharyaschev (1997), §16.7
  15. Rybakov (1997), Thm. 3.2.2
  16. Rybakov (1997), §3.5
  17. Jeřábek (2007)
  18. Chagrov & Zakharyaschev (1997), §18.5
  19. Ghilardi (2000), Thm. 2.2
  20. Ghilardi (2000), p. 196
  21. Ghilardi (2000), Thm. 3.6
  22. Rybakov (1997), Def. 1.4.13
  23. Mints & Kojevnikov (2004)
  24. Rybakov (1997), Thm. 4.5.5
  25. Rybakov (1997), §4.2
  26. Jeřábek (2008)
  27. Rybakov (1997), Cor. 4.3.20
  28. Iemhoff (2001, 2005), Rozière (1992)
  29. Jeřábek (2005)
  30. Jeřábek (2005,2008)
  31. Iemhoff (2001), Jeřábek (2005)
  32. Rybakov (1997), Thms. 5.5.6, 5.5.9
  33. Prucnal (1976)
  34. Rybakov (1997), §6.1
  35. Jeřábek (2005); cf. Kracht (2007), §7
  36. Jeřábek (2005, 2007, 2008)

References

This article is issued from Wikipedia - version of the Wednesday, March 30, 2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.