Inference Rule
A set of inference rules is called a calculus or inference system for a Logical System.
A logical system can have a formal language , then Inference Rules over that language are a decidable relation. Such rules can be written as:
where the are called assumptions and is called its conclusion.
No assumptions → Axiom.
An inference rule is called admissible in a calculus if the extension of the calculus by that rule does not yield any new theorems. This means all derivable inference rules are admissible as we can always use the rules that were used for the derivation. This does not hold the other way around.