Editing Admissible rule (section)

{{about|rules of inference in logic systems|the concept in [[decision theory]]|admissible decision rule|the solution substitution of a system of symbolic equations|Unification (computer science)}}

In [[logic]], a [[rule of inference]] is '''admissible''' in a [[formal system]] if the set of [[theorem]]s of the system does not change when that rule is added to the existing rules of the system. In other words, every [[well-formed formula|formula]] that can be [[formal proof|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).