An inference rule is admissible in a given proof calculus if it is possible to model applications of the inference rule by means of composition of other rules in the calculus. The cut-elimination theorem, fundamental to structural proof theory, states that the cut rule is admissible.
