Rule of inference
|
|
In logic, especially in mathematical logic, a rule of inference is a scheme for constructing valid inferences. These schemes establish syntactic relations between a set of formulas called premises and an assertion called a conclusion. These syntactic relations are used in the process of inference, whereby new true assertions are arrived at from other already known ones. Rules also apply to informal logic and arguments, but the formulation is much more difficult and controversial.
As stated, the application of a rule of inference is a purely syntactic procedure. Nevertheless it must also be valid, or more precisely validity preserving. In order for the requirement of validity preservation to make sense, some form of semantics is necessary for the assertions the rule of inference relates and the rule of inference itself. For a discussion of the interrelation between rules of inference and semantics, see the article on propositional logic.
Prominent examples of rules of inference in propositional logic are the rules of modus ponens and modus tollens. For first-order predicate logic, rules of inference are needed to deal with logical quantifiers. 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 case of first order predicate logic.
Note that there are many different systems of formal logic each one with its own set of well-formed formulas, rules of inference and semantics. See for instance temporal logic, modal logic, or intuitionistic logic. Quantum logic is also a form of logic quite different from the ones mentioned earlier. See also proof theory. In predicate calculus, an additional inference rule is needed. It is called Generalization.
In the setting of formal logic (and many related areas), 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 rule modus ponens of propositional logic. Rules of inference are usually formulated as rule schemata by the use of universal variables. In the rule (schema) above, A and B can be instantiated to any element of the universe (or sometimes, by convention, some restricted subset such as propositions) to form an infinite set of inference rules.
A proof system is formed from a set of rules, which can be chained together to form proofs, or derivations. Any derivation has only one final conclusion, which is the statement proved or derived. If premises are left unsatisfied in the derivation, then the derivation is a proof of a hypothetical statement: "if the premises hold, then the conclusion holds."
Admissibility and Derivability
In a set of rules, an inference rule could be redundant in the sense that it is admissible or derivable. A derivable rule is one whose conclusion can be derived from its premises using the other rules. An admissible rule is one whose conclusion holds whenever the premises hold. All derivable rules are admissible. To appreciate the difference, consider the following set of rules for defining the natural numbers (the judgment <math>n\,\,\mathsf{nat}<math> asserts the fact that <math>n<math> is a natural number):
<math> \begin{matrix} \frac{}{\mathbf{0} \,\,\mathsf{nat}} & \frac{n \,\,\mathsf{nat}}{\mathbf{s(}n\mathbf{)} \,\,\mathsf{nat}} \\ \end{matrix} <math>
The first rule states that 0 is a natural number, and the second states that s(n) is a natural number if n is. In this proof system, the following rule demonstrating that the second successor of a natural number is also a natural number, is derivable:
<math> \frac{n \,\,\mathsf{nat}}{\mathbf{s(s(}n\mathbf{))} \,\,\mathsf{nat}} <math>
Its derivation is just the composition of two uses of the successor rule above. The following rule for asserting the existence of a predecessor for any nonzero number is merely admissible:
<math> \frac{\mathbf{s(}n\mathbf{)} \,\,\mathsf{nat}}{n \,\,\mathsf{nat}} <math>
This is a true fact of natural numbers, as can be proven by induction. (To prove that this rule is admissible, one would assume a derivation of the premise, and induct on it to produce a derivation of <math>n \,\,\mathsf{nat}<math>.) However, it is not derivable, because it depends on the structure of the derivation of the premise. Because of this derivability is stable under additions to the proof system, whereas admissibility is not. To see the difference, suppose the following nonsense rule were added to the proof system:
<math> \frac{}{\mathbf{s(-3)} \,\,\mathsf{nat}} <math>
In this new system, the double-successor rule is still derivable. However, the rule for finding the predecessor is no longer admissible, because there is no way to derive <math>\mathbf{-3} \,\,\mathsf{nat}<math>. The brittleness of admissibility comes from the way it is proved: since the proof can induct on the structure of the derivations of the premises, extensions to the system add new cases to this proof, which may no longer hold.
Admissible rules can be thought of as theorems of a proof system. For instance, in a sequent calculus where cut elimination holds, the cut rule is admissible.
Other Considerations
Inference rules may also be stated in this form: (1) some (perhaps zero) premises, (2) a turnstile symbol <math> \vdash <math> which means "infers", "proves" or "concludes", (3) a conclusion. The turnstile symbolizes the executive power. The implication symbol <math> \rightarrow <math> has no such power: it only indicates potential inference. <math> \rightarrow <math> is another logical operator, it operates on truth values. <math> \vdash <math> is not a logical operator. It is rather a catalyst which metabolizes true statements to create new statements.
Rules of inference must be distinguished from axioms of a theory, which are assertions that are assumed to be true without proof. In terms of semantics, axioms are valid assertions. Axioms are usually regarded as starting points for applying rules of inference and generating a set of conclusions. Note that there is no sharp distinction between a rule of inference and an axiom, in the sense that a rule can be artificially encoded as an axiom and vice-versa. For instance, the set premises of a rule could be void, so that the conclusion is always true. Conversely, an axiom is commonly supposed to be a single clause, but in fact one could specify a schema 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 and natural deduction.