Rule of inference

In logic, especially in mathematical logic, a rule of inference might be any instruction of how some statement may be logically concluded from other given statements that are assumed to be true. As such it has to be quite precise and thus usually is given in some formal way.

Prominent examples of this concept are the rules of modus ponens and modus tollens. See also validity for more information on the informal description of such arguments.

In the formal setting of proof theory (and many related areas), however, rules of inference are usually given in the following standard form:

  Premise#1 Premise#2 ... Premise#n   
  Conclusion

This expression states, that whenever in the course of some logical derivation the given premisses have been obtained, the specified conclusion can be taken for granted as well. The exact formal language that is used to describe both premisses and conclusions depends on the actual context of the derivations. In a simple case, one may use logical formulae, such as in

  A→B   A   
  B

which is just the regular modus ponens. Here, one may usually assume that the rule actually is a rule scheme that encodes (infinitely) many other rules. In fact, one might use arbitrary formulae in place of A and B and the rule would still be valid.

A special form of a rule of inference is obtained if no premisses are given at all. In this case, the consequence may be concluded without further assumptions, i.e. it is an axiom.

Rules of inference play a vital role in the specification of logical calculi as they are considered in proof theory, such as the sequent calculus.