In a deductive system $\text{L}$, describes any rule of inference that can be ‘emulated’ by the remaining rules and axioms. This is to say that a rule is admissible in a deductive system if for every formula $\psi$ provable by appeal to that rule, there exists a proof in which the rule is not employed. The admissibility of inference rules is frequently examined in formal logic. For example, that the cut rule is admissible in a sequent calculus—that it admits cut elimination—is often an important intermediate step in proving that the calculus enjoys further properties.