# Admissible rule

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/Admissible_rule
> Markdown URL: https://mediated.wiki/source/Admissible_rule.md
> Source: https://en.wikipedia.org/wiki/Admissible_rule
> Source revision: 1348022866
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

This article is about rules of inference in logic systems. For the concept in [decision theory](/source/Decision_theory), see [admissible decision rule](/source/Admissible_decision_rule). For the solution substitution of a system of symbolic equations, see [Unification (computer science)](/source/Unification_(computer_science)).

In [logic](/source/Logic), a [rule of inference](/source/Rule_of_inference) is **admissible** in a [formal system](/source/Formal_system) if the set of [theorems](/source/Theorem) of the system does not change when that rule is added to the existing rules of the system. In other words, every [formula](/source/Well-formed_formula) that can be [derived](/source/Formal_proof) 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](/source/Paul_Lorenzen) (1955).

## Definitions

Admissibility has been systematically studied only in the case of structural (i.e. [substitution](/source/Substitution_(logic))-closed) rules in [propositional](/source/Propositional_logic) [non-classical logics](/source/Non-classical_logic), which we will describe next.

Let a set of basic [propositional connectives](/source/Logical_connective) be fixed (for instance, { → , ∧ , ∨ , ⊥ } {\displaystyle \{\to ,\land ,\lor ,\bot \}} in the case of [superintuitionistic logics](/source/Superintuitionistic_logic), or { → , ⊥ , ◻ } {\displaystyle \{\to ,\bot ,\Box \}} in the case of [monomodal logics](/source/Modal_logic)). [Well-formed formulas](/source/Well-formed_formulas) are built freely using these connectives from a [countably infinite](/source/Countable_set) set of [propositional variables](/source/Propositional_variable) *p*0, *p*1, .... A [substitution](/source/Substitution_(logic)) *σ* is a function from formulas to formulas that commutes with applications of the connectives, i.e.,

- σ f ( A 1 , … , A n ) = f ( σ A 1 , … , σ A n ) {\displaystyle \sigma f(A_{1},\dots ,A_{n})=f(\sigma A_{1},\dots ,\sigma A_{n})}

for every connective *f*, and formulas *A*1, ... , *A**n*. (We may also apply substitutions to sets Γ of formulas, making *σ*Γ = {*σA*: *A* ∈ Γ}.) A Tarski-style [consequence relation](/source/Consequence_relation)[1] is a relation ⊢ {\displaystyle \vdash } between sets of formulas, and formulas, such that

1. A ⊢ A , {\displaystyle A\vdash A,}
1. if Γ ⊢ A {\displaystyle \Gamma \vdash A} then Γ , Δ ⊢ A , {\displaystyle \Gamma ,\Delta \vdash A,} ("weakening")
1. if Γ ⊢ A {\displaystyle \Gamma \vdash A} and Δ , A ⊢ B {\displaystyle \Delta ,A\vdash B} then Γ , Δ ⊢ B , {\displaystyle \Gamma ,\Delta \vdash B,} ("composition")

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

1. if Γ ⊢ A {\displaystyle \Gamma \vdash A} then σ Γ ⊢ σ A {\displaystyle \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](/source/Structural_rule) in [sequent calculi](/source/Sequent_calculus).) A structural consequence relation is called a **propositional logic**. A formula *A* is a theorem of a logic ⊢ {\displaystyle \vdash } if ∅ ⊢ A {\displaystyle \varnothing \vdash A} .

For example, we identify a superintuitionistic logic *L* with its standard consequence relation ⊢ L {\displaystyle \vdash _{L}} generated by [modus ponens](/source/Modus_ponens) and axioms, and we identify a [normal modal logic](/source/Normal_modal_logic) with its global consequence relation ⊢ L {\displaystyle \vdash _{L}} generated by modus ponens, necessitation, and (as axioms) the theorems of the logic.

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

- A 1 , … , A n B or A 1 , … , A n / B , {\displaystyle {\frac {A_{1},\dots ,A_{n}}{B}}\qquad {\text{or}}\qquad A_{1},\dots ,A_{n}/B,}

where Γ = {*A*1, ... , *A**n*} is a finite set of formulas, and *B* is a formula. An **instance** of the rule is

- σ A 1 , … , σ A n / σ B {\displaystyle \sigma A_{1},\dots ,\sigma A_{n}/\sigma B}

for a substitution *σ*. The rule Γ/*B* is **derivable** in ⊢ {\displaystyle \vdash } , if Γ ⊢ B {\displaystyle \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 it, when added to the logic, does not lead to new theorems.[4] We also write Γ | ∼ B {\displaystyle \Gamma \mathrel {|\!\!\!\sim } B} if Γ/*B* is admissible. (Note that . | ∼ {\displaystyle {\phantom {.}}\!{|\!\!\!\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., ⊢ = | ∼ {\displaystyle {\vdash }={\,|\!\!\!\sim }} .[5]

In logics with a well-behaved [conjunction](/source/Logical_conjunction) connective (such as superintuitionistic or modal logics), a rule A 1 , … , A n / B {\displaystyle A_{1},\dots ,A_{n}/B} is equivalent to A 1 ∧ ⋯ ∧ A n / B {\displaystyle A_{1}\land \dots \land A_{n}/B} with respect to admissibility and derivability. It is therefore customary to only deal with [unary](/source/Unary_operation) rules *A*/*B*.

## Examples

- [Classical propositional calculus](/source/Classical_logic) (*CPC*) is structurally complete.[6] Indeed, assume that *A*/*B* is a non-derivable rule, and fix an assignment *v* such that *v*(*A*) = 1, and *v*(*B*) = 0. Define a substitution *σ* such that for every variable *p*, *σp* = ⊤ {\displaystyle \top } if *v*(*p*) = 1, and *σp* = ⊥ {\displaystyle \bot } if *v*(*p*) = 0. Then *σA* is a theorem, but *σB* is not (in fact, ¬*σB* is a theorem). Thus the rule *A*/*B* is not admissible either. (The same argument applies to any [multi-valued logic](/source/Multi-valued_logic) *L* complete with respect to a [logical matrix](/source/Logical_matrix) all of whose elements have a name in the language of *L*.)

- The [Kreisel](/source/Georg_Kreisel)–[Putnam](/source/Hilary_Putnam) rule (also known as [Harrop](https://en.wikipedia.org/w/index.php?title=Ronald_Harrop&action=edit&redlink=1)'s rule, or [independence of premise](/source/Independence_of_premise) rule)

- - ( K P R ) ¬ p → q ∨ r ( ¬ p → q ) ∨ ( ¬ p → r ) {\displaystyle ({\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](/source/Intuitionistic_logic) (*IPC*). In fact, it is admissible in every superintuitionistic logic.[7] On the other hand, the formula - ( ¬ p → q ∨ r ) → ( ( ¬ p → q ) ∨ ( ¬ p → r ) ) {\displaystyle (\neg p\to q\lor r)\to ((\neg p\to q)\lor (\neg p\to r))}

- is not an intuitionistic theorem; hence *KPR* is not derivable in *IPC*. In particular, *IPC* is not structurally complete.

- The rule

- - ◻ p p {\displaystyle {\frac {\Box p}{p}}}

- is admissible in many modal logics, such as *K*, *D*, *K*4, *S*4, *GL* (see [this table](/source/Kripke_semantics#Correspondence_and_completeness) for names of modal logics). It is derivable in *S*4, but it is not derivable in *K*, *D*, *K*4, or *GL*.

- The rule

- - ◊ p ∧ ◊ ¬ p ⊥ {\displaystyle {\frac {\Diamond p\land \Diamond \neg p}{\bot }}}

- is admissible in normal logic L ⊇ S 4.3 {\displaystyle L\supseteq S4.3} .[8] It is derivable in *GL* and *S*4.1, but it is not derivable in *K*, *D*, *K*4, *S*4, or *S*5.

- [Löb's rule](/source/L%C3%B6b's_theorem)

- - ( L R ) ◻ p → p p {\displaystyle ({\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 *K*4. In particular, it is *not* true in general that a rule admissible in a logic *L* must be admissible in its extensions.

- The [Gödel–Dummett logic](/source/Intermediate_logic) (*LC*), and the modal logic *Grz*.3 are structurally complete.[9] The [product fuzzy logic](/source/T-norm_fuzzy_logics) is also structurally complete.[10]

## Decidability and reduced rules

The basic question about admissible rules of a given logic is whether the set of all admissible rules is [decidable](/source/Decidable_set). Note that the problem is nontrivial even if the logic itself (i.e., its set of theorems) is [decidable](/source/Decidability_(logic)): the definition of admissibility of a rule *A*/*B* involves an unbounded [universal quantifier](/source/Universal_quantifier) over all propositional substitutions. Hence *a priori* we only know that admissibility of rule in a decidable logic is Π 1 0 {\displaystyle \Pi _{1}^{0}} (i.e., its complement is [recursively enumerable](/source/Recursively_enumerable)). For instance, it is known that admissibility in the bimodal logics *K**u* and *K*4*u* (the extensions of *K* or *K*4 with the [universal modality](https://en.wikipedia.org/w/index.php?title=Universal_modality&action=edit&redlink=1)) is undecidable.[11] Remarkably, decidability of admissibility in the basic modal logic *K* is a major [open problem](/source/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](/source/Transitive_relation) modal logics were constructed by [Rybakov](https://en.wikipedia.org/w/index.php?title=Vladimir_V._Rybakov&action=edit&redlink=1), using the **reduced form of rules**.[12] A modal rule in variables *p*0, ... , *p**k* is called reduced if it has the form

- ⋁ i = 0 n ( ⋀ j = 0 k ¬ i , j 0 p j ∧ ⋀ j = 0 k ¬ i , j 1 ◻ p j ) p 0 , {\displaystyle {\frac {\bigvee _{i=0}^{n}{\bigl (}\bigwedge _{j=0}^{k}\neg _{i,j}^{0}p_{j}\land \bigwedge _{j=0}^{k}\neg _{i,j}^{1}\Box p_{j}{\bigr )}}{p_{0}}},}

where each ¬ i , j u {\displaystyle \neg _{i,j}^{u}} is either blank, or [negation](/source/Logical_negation) ¬ {\displaystyle \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](/source/If_and_only_if) it admits (or derives) *s*, by introducing [extension variables](https://en.wikipedia.org/w/index.php?title=Extension_variable&action=edit&redlink=1) for all subformulas in *A*, and expressing the result in the full [disjunctive normal form](/source/Disjunctive_normal_form). It is thus sufficient to construct a decision algorithm for admissibility of reduced rules.

Let ⋁ i = 0 n φ i / p 0 {\displaystyle \textstyle \bigvee _{i=0}^{n}\varphi _{i}/p_{0}} be a reduced rule as above. We identify every conjunction φ i {\displaystyle \varphi _{i}} with the set { ¬ i , j 0 p j , ¬ i , j 1 ◻ p j ∣ j ≤ k } {\displaystyle \{\neg _{i,j}^{0}p_{j},\neg _{i,j}^{1}\Box p_{j}\mid j\leq k\}} of its conjuncts. For any subset *W* of the set { φ i ∣ i ≤ n } {\displaystyle \{\varphi _{i}\mid i\leq n\}} of all conjunctions, let us define a [Kripke model](/source/Kripke_model) M = ⟨ W , R , ⊩ ⟩ {\displaystyle M=\langle W,R,{\Vdash }\rangle } by

- φ i ⊩ p j ⟺ p j ∈ φ i , {\displaystyle \varphi _{i}\Vdash p_{j}\iff p_{j}\in \varphi _{i},}

- φ i R φ i ′ ⟺ ∀ j ≤ k ( ◻ p j ∈ φ i ⇒ { p j , ◻ p j } ⊆ φ i ′ ) . {\displaystyle \varphi _{i}\,R\,\varphi _{i'}\iff \forall j\leq 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 *K*4:[13]

**Theorem**. The rule ⋁ i = 0 n φ i / p 0 {\displaystyle \textstyle \bigvee _{i=0}^{n}\varphi _{i}/p_{0}} is *not* admissible in *K*4 if and only if there exists a set W ⊆ { φ i ∣ i ≤ n } {\displaystyle W\subseteq \{\varphi _{i}\mid i\leq n\}} such that

1. φ i ⊮ p 0 {\displaystyle \varphi _{i}\nVdash p_{0}} for some i ≤ n , {\displaystyle i\leq n,}

1. φ i ⊩ φ i {\displaystyle \varphi _{i}\Vdash \varphi _{i}} for every i ≤ n , {\displaystyle i\leq n,}

1. for every subset *D* of *W* there exist elements α , β ∈ W {\displaystyle \alpha ,\beta \in W} such that the equivalences

- - α ⊩ ◻ p j {\displaystyle \alpha \Vdash \Box p_{j}} if and only if φ ⊩ p j ∧ ◻ p j {\displaystyle \varphi \Vdash p_{j}\land \Box p_{j}} for every φ ∈ D {\displaystyle \varphi \in D} - α ⊩ ◻ p j {\displaystyle \alpha \Vdash \Box p_{j}} if and only if α ⊩ p j {\displaystyle \alpha \Vdash p_{j}} and φ ⊩ p j ∧ ◻ p j {\displaystyle \varphi \Vdash p_{j}\land \Box p_{j}} for every φ ∈ D {\displaystyle \varphi \in D}

- hold for all *j*.

Similar criteria can be found for the logics *S*4, *GL*, and *Grz*.[14] Furthermore, admissibility in intuitionistic logic can be reduced to admissibility in *Grz* using the [Gödel–McKinsey–Tarski translation](/source/Modal_companion):[15]

- A | ∼ I P C B {\displaystyle A\,|\!\!\!\sim _{IPC}B} if and only if T ( A ) | ∼ G r z T ( B ) . {\displaystyle 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 *K*4 or *IPC*) modal and superintuitionistic logics, including e.g. *S*4.1, *S*4.2, *S*4.3, *KC*, *T**k* (as well as the above-mentioned logics *IPC*, *K*4, *S*4, *GL*, *Grz*).[16]

Despite being decidable, the admissibility problem has relatively high [computational complexity](/source/Computational_complexity_theory), even in simple logics: admissibility of rules in the basic transitive logics *IPC*, *K*4, *S*4, *GL*, *Grz* is [coNEXP](/source/NEXP)-complete.[17] This should be contrasted with the derivability problem (for rules or formulas) in these logics, which is [PSPACE](/source/PSPACE)-complete.[18]

## Projectivity and unification

Admissibility in propositional logics is closely related to unification in the [equational theory](/source/Equational_theory) of [modal](/source/Modal_algebra) or [Heyting algebras](/source/Heyting_algebra). The connection was developed by Ghilardi (1999, 2000). In the logical setup, a **unifier** of a formula *A* in the language of 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

- ⊢ L σ p ↔ υ τ p {\displaystyle \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](/source/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 that have a most general unifier are the **projective formulas**: these are formulas *A* such that there exists a unifier *σ* of *A* such that

- A ⊢ L B ↔ σ B {\displaystyle A\vdash _{L}B\leftrightarrow \sigma B}

for every formula *B*. Note that *σ* is an MGU of *A*. In transitive modal and superintuitionistic logics with the [finite model property](/source/Kripke_semantics#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](/source/Singleton_(mathematics)), 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*, *K*4, *S*4, *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

1. P ⊢ L A {\displaystyle P\vdash _{L}A} for every P ∈ Π ( A ) , {\displaystyle P\in \Pi (A),}

1. 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 | ∼ L B {\displaystyle P\,|\!\!\!\sim _{L}B} if and only if P ⊢ L B {\displaystyle P\vdash _{L}B}

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

- A | ∼ L B {\displaystyle A\,|\!\!\!\sim _{L}B} if and only if ∀ P ∈ Π ( A ) ( P ⊢ L B ) . {\displaystyle \forall P\in \Pi (A)\,(P\vdash _{L}B).}

## Bases of admissible rules

Let *L* be a logic. A set *R* of *L*-admissible rules 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 . | ∼ L {\displaystyle {\phantom {.}}\!{|\!\!\!\sim _{L}}} is the smallest structural consequence relation that includes ⊢ L {\displaystyle \vdash _{L}} and *R*.

Notice that decidability of admissible rules of a decidable logic is equivalent to the existence of recursive (or [recursively enumerable](/source/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](/source/Algorithm): we start in parallel two [exhaustive searches](/source/Exhaustive_search), one for a substitution *σ* that unifies *A* but not *B*, and one for a derivation of *A*/*B* from *R* and ⊢ L {\displaystyle \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](/source/Proof_complexity).[23]

For a given logic, we can ask whether it has a recursive or [finite](/source/Finite_set) 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](https://en.wikipedia.org/w/index.php?title=Tabular_logic&action=edit&redlink=1) 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*, *K*4, *S*4, *GL*, *Grz* do not have a finite basis of admissible rules,[25] though they have independent bases.[26]

### 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[27]

- - ◊ p ∧ ◊ ¬ p ⊥ . {\displaystyle {\frac {\Diamond p\land \Diamond \neg p}{\bot }}.}

- [Visser](https://en.wikipedia.org/w/index.php?title=Albert_Visser&action=edit&redlink=1) [[nl](https://nl.wikipedia.org/wiki/Albert_Visser)]'s rules

- - ( ⋀ i = 1 n ( p i → q i ) → p n + 1 ∨ p n + 2 ) ∨ r ⋁ j = 1 n + 2 ( ⋀ i = 1 n ( p i → q i ) → p j ) ∨ r , n ≥ 1 {\displaystyle {\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\geq 1}

- are a basis of admissible rules in *IPC* or *KC*.[28]

- The rules

- - ◻ ( ◻ q → ⋁ i = 1 n ◻ p i ) ∨ ◻ r ⋁ i = 1 n ◻ ( q ∧ ◻ q → p i ) ∨ r , n ≥ 0 {\displaystyle {\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\geq 0}

- are a basis of admissible rules of *GL*.[29] (Note that the empty disjunction is defined as ⊥ {\displaystyle \bot } .)

- The rules

- - ◻ ( ◻ ( q → ◻ q ) → ⋁ i = 1 n ◻ p i ) ∨ ◻ r ⋁ i = 1 n ◻ ( ◻ q → p i ) ∨ r , n ≥ 0 {\displaystyle {\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\geq 0}

- are a basis of admissible rules of *S*4 or *Grz*.[30]

## Semantics for admissible rules

A rule Γ/*B* is **valid** in a modal or intuitionistic [Kripke frame](/source/Kripke_frame) F = ⟨ W , R ⟩ {\displaystyle F=\langle W,R\rangle } , if the following is true for every valuation ⊩ {\displaystyle \Vdash } in *F*:

- if for all A ∈ Γ {\displaystyle A\in \Gamma } ∀ x ∈ W ( x ⊩ A ) {\displaystyle \forall x\in W\,(x\Vdash A)} , then ∀ x ∈ W ( x ⊩ B ) {\displaystyle \forall x\in W\,(x\Vdash B)} .

(The definition readily generalizes to [general frames](/source/General_frame), if needed.)

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

- a **reflexive tight predecessor** of *X*, if for every *y* in *W*: *t R y* if and only if *t* = *y* or for some *x* in *X*: *x* = *y* or *x R y* ,

- an **irreflexive tight predecessor** of *X*, if for every *y* in *W*: *t R y* if and only if for some *x* in *X*: *x* = *y* or *x R y* .

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]

- a rule is admissible in *IPC* if and only if it is valid in all intuitionistic frames that have reflexive tight predecessors,

- a rule is admissible in *K*4 if and only if it is valid in all [transitive](/source/Transitive_relation) frames that have reflexive and irreflexive tight predecessors,

- a rule is admissible in *S*4 if and only if it is valid in all transitive [reflexive](/source/Reflexive_relation) frames that have reflexive tight predecessors,

- a rule is admissible in *GL* if and only if it is valid in all transitive converse [well-founded](/source/Well-founded_relation) frames that have irreflexive tight predecessors.

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](/source/Grigori_Mints) rule

- ( p → q ) → p ∨ r ( ( p → q ) → p ) ∨ ( ( p → q ) → r ) {\displaystyle {\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 any 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 respectively 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 *K*4 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](/source/Intermediate_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

- A ( p 1 , … , p n , s 1 , … , s k ) B ( p 1 , … , p n , s 1 , … , s k ) , {\displaystyle {\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 *p**i*, and the parameters *s**i*. The rule is *L*-admissible if every *L*-unifier *σ* of *A* such that *σs**i* = *s**i* 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

- A 1 , … , A n B 1 , … , B m or A 1 , … , A n / B 1 , … , B m . {\displaystyle {\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](/source/Consistent) iff it admits the rule

- ⊥ , {\displaystyle {\frac {\;\bot \;}{}},}

and a superintuitionistic logic has the [disjunction property](/source/Disjunction_property) iff it admits the rule

- p ∨ q p , q . {\displaystyle {\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 *S*4 the rule above is equivalent to

- A 1 , … , A n ◻ B 1 ∨ ⋯ ∨ ◻ B m . {\displaystyle {\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](/source/Proof_theory), admissibility is often considered in the context of [sequent calculi](/source/Sequent_calculus), where the basic objects are sequents rather than formulas. For example, one can rephrase the [cut-elimination theorem](/source/Cut-elimination_theorem) as saying that the cut-free sequent calculus admits the [cut rule](/source/Cut_rule)

- Γ ⊢ A , Δ Π , A ⊢ Λ Γ , Π ⊢ Δ , Λ . {\displaystyle {\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 that we obtain by translating each sequent Γ ⊢ Δ {\displaystyle \Gamma \vdash \Delta } to its characteristic formula ⋀ Γ → ⋁ Δ {\displaystyle \bigwedge \Gamma \to \bigvee \Delta } .

## See also

- [Extension by new constant and function names](/source/Extension_by_new_constant_and_function_names)

- [Conservative extension](/source/Conservative_extension)

## Notes

1. **[^](#cite_ref-1)** Blok & Pigozzi (1989), Kracht (2007)

1. **[^](#cite_ref-2)** Rybakov (1997), Def. 1.1.3

1. **[^](#cite_ref-3)** Rybakov (1997), Def. 1.7.2

1. **[^](#cite_ref-4)** [From de Jongh’s theorem to intuitionistic logic of proofs](http://www.illc.uva.nl/D65/artemov.pdf)

1. **[^](#cite_ref-5)** Rybakov (1997), Def. 1.7.7

1. **[^](#cite_ref-6)** Chagrov & Zakharyaschev (1997), Thm. 1.25

1. **[^](#cite_ref-7)** Prucnal (1979), cf. Iemhoff (2006)

1. **[^](#cite_ref-8)** Rybakov (1997), p. 439

1. ^ [***a***](#cite_ref-hsc_9-0) [***b***](#cite_ref-hsc_9-1) [***c***](#cite_ref-hsc_9-2) Rybakov (1997), Thms. 5.4.4, 5.4.8

1. **[^](#cite_ref-10)** Cintula & Metcalfe (2009)

1. **[^](#cite_ref-11)** Wolter & Zakharyaschev (2008)

1. **[^](#cite_ref-12)** Rybakov (1997), §3.9

1. **[^](#cite_ref-13)** Rybakov (1997), Thm. 3.9.3

1. **[^](#cite_ref-14)** Rybakov (1997), Thms. 3.9.6, 3.9.9, 3.9.12; cf. Chagrov & Zakharyaschev (1997), §16.7

1. **[^](#cite_ref-15)** Rybakov (1997), Thm. 3.2.2

1. **[^](#cite_ref-16)** Rybakov (1997), §3.5

1. **[^](#cite_ref-17)** Jeřábek (2007)

1. **[^](#cite_ref-18)** Chagrov & Zakharyaschev (1997), §18.5

1. **[^](#cite_ref-19)** Ghilardi (2000), Thm. 2.2

1. **[^](#cite_ref-20)** Ghilardi (2000), p. 196

1. **[^](#cite_ref-21)** Ghilardi (2000), Thm. 3.6

1. **[^](#cite_ref-22)** Rybakov (1997), Def. 1.4.13

1. **[^](#cite_ref-23)** Mints & Kojevnikov (2004)

1. **[^](#cite_ref-24)** Rybakov (1997), Thm. 4.5.5

1. **[^](#cite_ref-25)** Rybakov (1997), §4.2

1. **[^](#cite_ref-26)** Jeřábek (2008)

1. **[^](#cite_ref-27)** Rybakov (1997), Cor. 4.3.20

1. **[^](#cite_ref-28)** Iemhoff (2001, 2005), Rozière (1992)

1. **[^](#cite_ref-29)** Jeřábek (2005)

1. **[^](#cite_ref-30)** Jeřábek (2005, 2008)

1. **[^](#cite_ref-31)** Iemhoff (2001), Jeřábek (2005)

1. **[^](#cite_ref-32)** Rybakov (1997), Thms. 5.5.6, 5.5.9

1. **[^](#cite_ref-33)** Prucnal (1976)

1. **[^](#cite_ref-34)** Rybakov (1997), §6.1

1. **[^](#cite_ref-35)** Jeřábek (2005); cf. Kracht (2007), §7

1. **[^](#cite_ref-36)** Jeřábek (2005, 2007, 2008)

## References

- W. Blok, D. Pigozzi, *Algebraizable logics*, [Memoirs of the American Mathematical Society](/source/Memoirs_of_the_American_Mathematical_Society) 77 (1989), no. 396, 1989.

- A. Chagrov and M. Zakharyaschev, *Modal Logic*, Oxford Logic Guides vol. 35, Oxford University Press, 1997. [ISBN](/source/ISBN_(identifier)) [0-19-853779-4](https://en.wikipedia.org/wiki/Special:BookSources/0-19-853779-4)

- P. Cintula and G. Metcalfe, *Structural completeness in fuzzy logics*, [Notre Dame Journal of Formal Logic](/source/Notre_Dame_Journal_of_Formal_Logic) 50 (2009), no. 2, pp. 153–182. [doi](/source/Doi_(identifier)):[10.1215/00294527-2009-004](https://doi.org/10.1215%2F00294527-2009-004)

- A. I. Citkin, *On structurally complete superintuitionistic logics*, Soviet Mathematics - Doklady, vol. 19 (1978), pp. 816–819.

- S. Ghilardi, *Unification in intuitionistic logic*, [Journal of Symbolic Logic](/source/Journal_of_Symbolic_Logic) 64 (1999), no. 2, pp. 859–880. [Project Euclid](http://projecteuclid.org/euclid.jsl/1183745815) [JSTOR](https://www.jstor.org/stable/view/2586506)

- S. Ghilardi, *Best solving modal equations*, [Annals of Pure and Applied Logic](/source/Annals_of_Pure_and_Applied_Logic) 102 (2000), no. 3, pp. 183–198. [doi](/source/Doi_(identifier)):[10.1016/S0168-0072(99)00032-9](https://doi.org/10.1016%2FS0168-0072%2899%2900032-9)

- [R. Iemhoff](/source/Rosalie_Iemhoff), *On the admissible rules of intuitionistic propositional logic*, Journal of Symbolic Logic 66 (2001), no. 1, pp. 281–294. [Project Euclid](http://projecteuclid.org/euclid.jsl/1183746371) [JSTOR](https://www.jstor.org/stable/view/2694922)

- R. Iemhoff, *Intermediate logics and Visser's rules*, Notre Dame Journal of Formal Logic 46 (2005), no. 1, pp. 65–81. [doi](/source/Doi_(identifier)):[10.1305/ndjfl/1107220674](https://doi.org/10.1305%2Fndjfl%2F1107220674)

- R. Iemhoff, *On the rules of intermediate logics*, [Archive for Mathematical Logic](/source/Archive_for_Mathematical_Logic), 45 (2006), no. 5, pp. 581–599. [doi](/source/Doi_(identifier)):[10.1007/s00153-006-0320-8](https://doi.org/10.1007%2Fs00153-006-0320-8)

- E. Jeřábek, *Admissible rules of modal logics*, [Journal of Logic and Computation](/source/Journal_of_Logic_and_Computation) 15 (2005), no. 4, pp. 411–431. [doi](/source/Doi_(identifier)):[10.1093/logcom/exi029](https://doi.org/10.1093%2Flogcom%2Fexi029)

- E. Jeřábek, *Complexity of admissible rules*, Archive for Mathematical Logic 46 (2007), no. 2, pp. 73–92. [doi](/source/Doi_(identifier)):[10.1007/s00153-006-0028-9](https://doi.org/10.1007%2Fs00153-006-0028-9)

- E. Jeřábek, *Independent bases of admissible rules*, Logic Journal of the IGPL 16 (2008), no. 3, pp. 249–267. [doi](/source/Doi_(identifier)):[10.1093/jigpal/jzn004](https://doi.org/10.1093%2Fjigpal%2Fjzn004)

- M. Kracht, *Modal Consequence Relations*, in: Handbook of Modal Logic (P. Blackburn, J. van Benthem, and F. Wolter, eds.), Studies of Logic and Practical Reasoning vol. 3, Elsevier, 2007, pp. 492–545. [ISBN](/source/ISBN_(identifier)) [978-0-444-51690-9](https://en.wikipedia.org/wiki/Special:BookSources/978-0-444-51690-9)

- P. Lorenzen, *Einführung in die operative Logik und Mathematik*, Grundlehren der mathematischen Wissenschaften vol. 78, Springer–Verlag, 1955.

- G. Mints and A. Kojevnikov, *Intuitionistic Frege systems are polynomially equivalent*, Zapiski Nauchnyh Seminarov POMI 316 (2004), pp. 129–146. [gzipped PS](http://www.emis.de/journals/ZPOMI/v316/p129.ps.gz)

- T. Prucnal, *Structural completeness of Medvedev's propositional calculus*, Reports on Mathematical Logic 6 (1976), pp. 103–105.

- T. Prucnal, *On two problems of Harvey Friedman*, [Studia Logica](/source/Studia_Logica) 38 (1979), no. 3, pp. 247–262. [doi](/source/Doi_(identifier)):[10.1007/BF00405383](https://doi.org/10.1007%2FBF00405383)

- P. Rozière, *Règles admissibles en calcul propositionnel intuitionniste*, Ph.D. thesis, [Université de Paris VII](/source/Universit%C3%A9_de_Paris_VII), 1992. [PDF](http://www.pps.jussieu.fr/~roziere/admiss/these.pdf)

- V. V. Rybakov, *Admissibility of Logical Inference Rules*, Studies in Logic and the Foundations of Mathematics vol. 136, Elsevier, 1997. [ISBN](/source/ISBN_(identifier)) [0-444-89505-1](https://en.wikipedia.org/wiki/Special:BookSources/0-444-89505-1)

- F. Wolter, M. Zakharyaschev, *Undecidability of the unification and admissibility problems for modal and description logics*, [ACM Transactions on Computational Logic](/source/ACM_Transactions_on_Computational_Logic) 9 (2008), no. 4, article no. 25. [doi](/source/Doi_(identifier)):[10.1145/1380572.1380574](https://doi.org/10.1145%2F1380572.1380574) [PDF](https://web.archive.org/web/20110718020147/http://tocl.acm.org/accepted/318wolter.pdf)

---
Adapted from the Wikipedia article [Admissible rule](https://en.wikipedia.org/wiki/Admissible_rule) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/Admissible_rule?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.