- Admissible rule
In

logic , arule of inference is**admissible**in aformal system if the set of theorems of the system is closed under the rule. The concept of an admissible rule was introduced byPaul Lorenzen (1955).**Definitions**The concept of admissibility, as introduced above, can be applied generally to formal systems which do not resemble any kind of logic, see this example. However, admissibility has been systematically studied only in the case of structural rules in propositional

non-classical logic s, which we will describe next.Let a set of basic propositional connectives be fixed (for instance, $\{\; o,land,lor,ot\}$ in the case of

superintuitionistic logic s, or $\{\; o,ot,Box\}$ in the case of monomodal logics).Well-formed formulas are built freely using these connectives from a countably infinite set ofpropositional variable s "p"_{"n"}. Asubstitution σ 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 "A"_{1}, …, "A"_{"n"}. (We may also apply substitutions to sets Γ of formulas, making nowrap|1=σΓ = {σ"A": "A" ∈ Γ}.) A Tarski-styleconsequence relation [*Blok & Pigozzi (1989), Kracht (2007)*] is a relation $vdash$ between sets of formulas, and formulas, such that

#$Avdash\; A,$

#if $Gammavdash\; A$ then $Gamma,Deltavdash\; A,$

#if $Gammavdash\; A$ and $Delta,Avdash\; B$ then $Gamma,Deltavdash\; B,$for all formulas "A", "B", and sets of formulas Γ, Δ. A consequence relation such that- if $Gammavdash\; A$ then $sigmaGammavdashsigma\; A$

**structural**. (Note that the term "structural" as used here and below is unrelated to the notion ofstructural rule s in sequent calculi.) A structural consequence relation is called a**propositional logic**. A formula "A" is atheorem of a logic $vdash$ if $varnothingvdash\; 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 anormal modal logic with its global consequence relation $vdash\_L$ axiomatized by modus ponens, necessitation, and axioms.A

**structural inference rule**[*Rybakov (1997), Def. 1.1.3*] (or just**rule**for short) is given by a pair (Γ,"B"), usually written as:$frac\{A\_1,dots,A\_n\}Bqquad\; ext\{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:$sigma\; A\_1,dots,sigma\; A\_n/sigma\; B$for a substitution σ. The rule Γ/"B" is**derivable**in $vdash$, if $Gammavdash\; B$. It is**admissible**if for every instance of the rule, σ"B" is a theorem whenever all formulas from σΓ are theorems. [*Rybakov (1997), Def. 1.7.2*] 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\}$. [*Rybakov (1997), Def. 1.7.7*]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\_1landdotsland\; A\_n/B$ with respect to admissibility and derivability. It is therefore customary to only deal with unary rules "A"/"B".

**Examples***Classical propositional calculus ("CPC") is structurally complete. [

*Chagrov & Zakharyaschev (1997), Thm. 1.25*] Indeed, assume that "A"/"B" is 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" = $op$ if "v"("p") = 1, and σ"p" = $ot$ 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 anymulti-valued logic "L" complete with respect to a logical matrix whose all elements have a name in the language of "L".)

*The Kreisel–Putnam rule (aka Harrop's rule, or independence of premise rule)::$(mathit\{KPR\})qquadfrac\{\; eg\; p\; o\; qlor\; r\}\{(\; eg\; p\; o\; q)lor(\; eg\; p\; o\; r)\}$:is admissible in the intuitionistic propositional calculus ("IPC"). In fact, it is admissible in every superintuitionistic logic. [*Prucnal (1979), cf. Iemhoff (2006)*] On the other hand, the formula::$(\; eg\; p\; o\; qlor\; r)\; o(\; eg\; p\; o\; q)lor(\; eg\; p\; o\; r)$:is not an intuitionistic tautology, hence "KPR" is not derivable in "IPC". In particular, "IPC" is not structurally complete.

*The rule::$frac\{Box\; p\}p$:is admissible in many modal logics, such as "K", "D", "K"4, "S"4, "GL" (see this table 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::$frac\{Diamond\; plandDiamond\; eg\; p\}ot$:is admissible in every normal modal logic. [*Rybakov (1997), p. 439*] It is derivable in "GL" and "S"4.1, but it is not derivable in "K", "D", "K"4, "S"4, "S"5.

*Löb's rule::$(mathit\{LR\})qquadfrac\{Box\; p\; o\; 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 ("LC"), and the modal logic "Grz".3 are structurally complete.Rybakov (1997), Thms. 5.4.4, 5.4.8]**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 now that admissibility of rule in a decidable logic is $Pi^0\_1$ (i.e., its complement isrecursively 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 theuniversal modality ) is undecidable. [*Wolter & Zakharyaschev (2008)*] 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**. [*Rybakov (1997), §3.9*] A modal rule in variables "p"_{0}, …, "p"_{"k"}is called reduced if it has the form:$frac\{igvee\_\{i=0\}^nigl(igwedge\_\{j=0\}^k\; eg\_\{i,j\}^0p\_jlandigwedge\_\{j=0\}^k\; eg\_\{i,j\}^1Box\; p\_jigr)\}\{p\_0\},$where each $eg\_\{i,j\}^u$ is either blank, or negation $eg$. 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 introducingextension variable s for all subformulas in "A", and expressing the result in the fulldisjunctive normal form . It is thus sufficient to construct a decision algorithm for admissibility of reduced rules.Let $extstyleigvee\_\{i=0\}^nvarphi\_i/p\_0$ be a reduced rule as above. We identify every conjunction $varphi\_i$ with the set $\{\; eg\_\{i,j\}^0p\_j,\; eg\_\{i,j\}^1Box\; p\_jmid\; jle\; k\}$ of its conjuncts. For any subset "W" of the set $\{varphi\_imid\; ile\; n\}$ of all conjunctions, let us define a

Kripke model $M=langle\; W,R,\{Vdash\}\; angle$ by:$varphi\_iVdash\; p\_jiff\; p\_jinvarphi\_i,$:$varphi\_i,R,varphi\_\{i\text{'}\}iffforall\; jle\; k,(Box\; p\_jinvarphi\_iRightarrow\{p\_j,Box\; p\_j\}subseteqvarphi\_\{i\text{'}\}).$ Then the following provides an algorithmic criterion for admissibility in "K"4: [*Rybakov (1997), Thm. 3.9.3*]**Theorem**. The rule $extstyleigvee\_\{i=0\}^nvarphi\_i/p\_0$ is "not" admissible in "K"4 if and only if there exists a set $Wsubseteq\{varphi\_imid\; ile\; n\}$ such that

#$varphi\_i\; Vdash\; p\_0$ for some $ile\; n,$

#$varphi\_iVdashvarphi\_i$ for every $ile\; n,$

#for every subset "D" of "W" there exist elements $alpha,etain\; W$ such that the equivalences::$alphaVdashBox\; p\_j$ if and only if $varphiVdash\; p\_jlandBox\; p\_j$ for every $varphiin\; D$::$alphaVdashBox\; p\_j$ if and only if $alphaVdash\; p\_j$ and $varphiVdash\; p\_jlandBox\; p\_j$ for every $varphiin\; D$:hold for all "j".Similar criteria can be found for the logics "S"4, "GL", and "Grz". [

*Rybakov (1997), Thms. 3.9.6, 3.9.9, 3.9.12; cf. Chagrov & Zakharyaschev (1997), §16.7*] Furthermore, admissibility in intuitionistic logic can be reduced to admissibility in "Grz" using the Gödel–McKinsey–Tarski translation: [*Rybakov (1997), Thm. 3.2.2*] :$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 "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"). [*Rybakov (1997), §3.5*]Despite being decidable, the admissibility problem has relatively high

computational complexity , even in simple logics: admissibility of rules in the basic transitive logics "IPC", "K"4, "S"4, "GL", "Grz" is coNEXP-complete. [*Jeřábek (2007)*] This should be contrasted with the derivability problem (for rules or formulas) in these logics, which isPSPACE -complete. [*Chagrov & Zakharyaschev (1997), §18.5*]**Projectivity and unification**Admissibility in propositional logics is closely related to

unification in theequational theory of modal orHeyting algebra s. 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\_Lsigma\; pleftrightarrow\; upsilon\; au\; 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". Amost 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:$Avdash\_L\; Bleftrightarrowsigma\; 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**: [*Ghilardi (2000), Thm. 2.2*] 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", "K"4, "S"4, "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"): [*Ghilardi (2000), p. 196*] a finite set of projective formulas such that

#$Pvdash\_L\; A$ for every $PinPi(A),$

#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 $Pvdash\_L\; B$for any formula "B". Thus we obtain the following effective characterization of admissible rules: [*Ghilardi (2000), Thm. 3.6*] :$A,|!!!sim\_L\; B$ if and only if $forall\; PinPi(A),(Pvdash\_L\; B).$**Bases of admissible rules**Let "L" be a logic. A set "R" of "L"-admissible rule is called a

basis [*Rybakov (1997), Def. 1.4.13*] 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 (orrecursively 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 followingalgorithm : we start in parallel twoexhaustive search es, 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. inproof complexity . [*Mints & Kojevnikov (2004)*]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 logic s are generally well-behaved, and always finitely axiomatizable, there exist tabular modal logics without a finite or independent basis of rules. [*Rybakov (1997), Thm. 4.5.5*] 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, [*Rybakov (1997), §4.2*] though they have independent bases. [*Jeřábek (2008)*]**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 [*Rybakov (1997), Cor. 4.3.20*] ::$frac\{Diamond\; plandDiamond\; eg\; p\}ot.$

*Visser's rules::$frac\{displaystyleBigl(igwedge\_\{i=1\}^n(p\_i\; o\; q\_i)\; o\; p\_\{n+1\}lor\; p\_\{n+2\}Bigr)lor\; r\}\{displaystyleigvee\_\{j=1\}^\{n+2\}Bigl(igwedge\_\{i=1\}^\{n\}(p\_i\; o\; q\_i)\; o\; p\_jBigr)lor\; r\},qquad\; nge\; 1$:are a basis of admissible rules in "IPC" or "KC". [*Iemhoff (2001, 2005), Roziere (1992)*]

*The rules::$frac\{displaystyleBoxBigl(Box\; q\; oigvee\_\{i=1\}^nBox\; p\_iBigr)lorBox\; r\}\{displaystyleigvee\_\{i=1\}^nBox(qlandBox\; q\; o\; p\_i)lor\; r\},qquad\; nge0$:are a basis of admissible rules of "GL". [*Jeřábek (2005)*] (Note that the empty disjunction is defined as $ot$.)

*The rules::$frac\{displaystyleBoxBigl(Box(q\; oBox\; q)\; oigvee\_\{i=1\}^nBox\; p\_iBigr)lorBox\; r\}\{displaystyleigvee\_\{i=1\}^nBox(Box\; q\; o\; p\_i)lor\; r\},qquad\; nge0$:are a basis of admissible rules of "S"4 or "Grz". [*Jeřábek (2005,2008)*]**emantics for admissible rules**A rule Γ/"B" is

**valid**in a modal or intuitionisticKripke frame $F=langle\; W,R\; angle$, if the following is true for every valuation $Vdash$ in "F"::if $forall\; xin\; W,(xVdash\; A)$ for all $AinGamma$, then $forall\; xin\; W,(xVdash\; B)$.(The definition readily generalizes togeneral frame s, 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 "x" = "y" or "x R y" for some "x" in "X",

*an**irreflexive tight predecessor**of "X", if for every "y" in "W": "t R y" if and only if "x" = "y" or "x R y" for some "x" in "X".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: [

*Iemhoff (2001), Jeřábek (2005)*]

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

*a rule is admissible in "K"4 if and only if it is valid in all transitive frames which have reflexive and irreflexive tight predecessors,

*a rule is admissible in "S"4 if and only if it is valid in all transitivereflexive frames which have reflexive tight predecessors,

*a rule is admissible in "GL" if and only if it is valid in all transitive converse well-founded frames which 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.

**tructural 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. [

*Rybakov (1997), Thms. 5.5.6, 5.5.9*] On the other hand, the Mints rule:$frac\{(p\; o\; q)\; o\; plor\; r\}\{((p\; o\; q)\; o\; p)lor((p\; o\; q)\; o\; 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 Tsitkin 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::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).There exist structurally complete logics that are not hereditarily structurally complete: for example, Medvedev's logic is structurally complete, [

*Prucnal (1976)*] 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 "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. [*Rybakov (1997), §6.1*]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\; ext\{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 Δ. [*Jeřábek (2005); cf. Kracht (2007), §7*] For example, a logic "L" isconsistent iff it admits the rule:$frac\{;ot;\}\{\},$and a superintuitionistic logic has thedisjunction property iff it admits the rule:$frac\{plor\; q\}\{p,q\}.$Again, basic results on admissible rules generalize smoothly to multiple-conclusion rules. [*Jeřábek (2005, 2007, 2008)*] 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:$frac\{A\_1,dots,A\_n\}\{Box\; B\_1lordotslorBox\; 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 thecut-elimination theorem as saying that the cut-free sequent calculus admits thecut rule :$frac\{Gammavdash\; A,DeltaqquadPi,AvdashLambda\}\{Gamma,DeltavdashPi,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 $GammavdashDelta$ to its characteristic formula $igwedgeGamma\; oigveeDelta$.**Notes****References***W. Blok, D. Pigozzi, "Algebraizable logics", 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 0-19-853779-4

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

*S. Ghilardi, "Best solving modal equations", Annals of Pure and Applied Logic 102 (2000), no. 3, pp. 183–198. doi|10.1016/S0168-0072(99)00032-9

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

*R. Iemhoff, "Intermediate logics and Visser's rules", Notre Dame Journal of Formal Logic 46 (2005), no. 1, pp. 65–81. doi|10.1305/ndjfl/1107220674

*R. Iemhoff, "On the rules of intermediate logics", Archive for Mathematical Logic, 45 (2006), no. 5, pp. 581–599. doi|10.1007/s00153-006-0320-8

*E. Jeřábek, "Admissible rules of modal logics", Journal of Logic and Computation 15 (2005), no. 4, pp. 411–431. doi|10.1093/logcom/exi029

*E. Jeřábek, "Complexity of admissible rules", Archive for Mathematical Logic 46 (2007), no. 2, pp. 73–92. doi|10.1007/s00153-006-0028-9

*E. Jeřábek, "Independent bases of admissible rules", Logic Journal of the IGPL, 2008, to appear. doi|10.1093/jigpal/jzn004

*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 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. [*http://www.emis.de/journals/ZPOMI/v316/p129.ps.gz gzipped PS*]

*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 38 (1979), no. 3, pp. 247–262. doi|10.1007/BF00405383

*P. Roziere, "Règles admissibles en calcul propositionnel intuitionniste", Ph.D. thesis, Université de Paris VII, 1992.

*V. V. Rybakov, "Admissibility of Logical Inference Rules", Studies in Logic and the Foundations of Mathematics vol. 136, Elsevier, 1997. ISBN 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 9 (2008), to appear. [*http://tocl.acm.org/accepted/318wolter.pdf PDF*]

*Wikimedia Foundation.
2010.*

### Look at other dictionaries:

**Admissible decision rule**— In classical (frequentist) decision theory, an admissible decision rule is a rule for making a decision that is better than any other rule that may compete with it, in a specific sense defined below. Generally speaking, in most decision problems… … Wikipedia**Rule of inference**— In logic, a rule of inference (also called a transformation rule) is a function from sets of formulae to formulae. The argument is called the premise set (or simply premises ) and the value the conclusion . They can also be viewed as relations… … Wikipedia**admissible**— ad·mis·si·ble /əd mi sə bəl, ad / adj: capable of being allowed or permitted the difficulty would be lessened if entries in books of account were admissible as prima facie evidence B. N. Cardozo ad·mis·si·bil·i·ty / ˌmi sə bi lə tē/ n Merriam… … Law dictionary**best evidence rule**— Rule which requires that best evidence available be presented in lieu of less satisfactory evidence. People v. Banks, Colo.App., 655 P.2d 1384, 1387. This rule prohibits the introduction into evidence of secondary evidence unless it is shown that … Black's law dictionary**best evidence rule**— Rule which requires that best evidence available be presented in lieu of less satisfactory evidence. People v. Banks, Colo.App., 655 P.2d 1384, 1387. This rule prohibits the introduction into evidence of secondary evidence unless it is shown that … Black's law dictionary**exclusionary rule**— n: any of various rules that exclude or suppress evidence; specif: a rule of evidence that excludes or suppresses evidence obtained in violation of a defendant s constitutional rights see also fruit of the poisonous tree, good faith exception,… … Law dictionary**hearsay rule**— n: a rule barring the admission of hearsay as evidence ◇ The hearsay rule is stated in Rule 802 of the Federal Rules of Evidence. Hearsay is inadmissible as evidence because of the unavailability of cross examination to test the accuracy of the… … Law dictionary**Best evidence rule**— The best evidence rule is a common law rule of evidence which can be traced back at least as far as the 18th century. In Omychund v Barker (1745) 1 Atk, 21, 49; 26 ER 15, 33, Lord Harwicke stated that no evidence was admissible unless it was the… … Wikipedia**exclusionary rule**— a rule that forbids the introduction of illegally obtained evidence in a criminal trial. [1955 60] * * * In U.S. law, the principle that evidence seized by police in violation of the constitutional protection against unreasonable search and… … Universalium**Dominating decision rule**— In decision theory, a decision rule is said to dominate another if the performance of the former is sometimes better, and never worse, than that of the latter. Formally, let δ1 and δ2 be two decision rules, and let R(θ,δ) be the risk of rule δ… … Wikipedia