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. And see first order resolution for a uniform treatment of all rules of inference as a single rule.

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 premises have been obtained, the specified conclusion can be taken for granted as well. The exact formal language that is used to describe both premises 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.

Rules of inference must be carefully distinguished from axioms, which are statements that are assumed to be true without proof, and are the starting points for applying the rules of inference. Rules of inference, on the other hand, are logically valid independent of any assumptions. This is important because both can have essentially the same form. A rule of inference is usually supposed to have both premise (antecedent) and conclusion (consequent), however, the antecedent could be the trivial one "true", which is no antecedent at all (the consequent is always true). Conversely, an axiom is commonly supposed to be a single clause, but in fact one could specify a production rule that generates an infinite set of axioms, which would superficially have the same form as a rule of inference.

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.