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).