Admissible rule

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

Admissibility has been systematically studied only in the case of structural rules in propositional non-classical logics, which we will describe next.

Let a set of basic propositional connectives be fixed (for instance, ${\displaystyle \{\to ,\land ,\lor ,\bot \}}$ in the case of superintuitionistic logics, or ${\displaystyle \{\to ,\bot ,\Box \}}$ in the case of monomodal logics). Well-formed formulas are built freely using these connectives from a countably infinite set of propositional variables p₀, p₁, …. A substitution σ is a function from formulas to formulas which commutes with the connectives, i.e.,

...
Wikipedia