Rules of inference

Assessment | Biopsychology | Comparative | Cognitive | Developmental | Language | Individual differences | Personality | Philosophy | Social |
Methods | Statistics | Clinical | Educational | Industrial | Professional items | World psychology |

Philosophy Index: Aesthetics · Epistemology · Ethics · Logic · Metaphysics · Consciousness · Philosophy of Language · Philosophy of Mind · Philosophy of Science · Social and Political philosophy · Philosophies · Philosophers · List of lists

---

Rules of inference
Propositional calculus
Modus ponens ·Modus tollens Modus ponendo tollens Conjunction introduction Simplification Disjunction introduction Disjunction elimination Disjunctive syllogism Hypothetical syllogism Constructive dilemma Destructive dilemma Biconditional introduction Biconditional elimination
Predicate calculus
Universal generalization Universal instantiation Existential generalization Existential instantiation
Documentation </noinclude>

In logic, a transformation rule or rule of inference is a syntactic rule or function which takes premises and returns a conclusion (or in multiple-conclusion logic, conclusions). For example, the rule of inference modus ponens takes two premises, one in the form of "If p then q" and another in the form of "p" and returns the conclusion "q". The rule is valid with respect to the semantics of classical logic (as well as the semantics of many other non-classical logics), in the sense that if the premises are true (under an interpretation) then so is the conclusion.

Typically a rule of inference preserves the semantic property of truth (or designationhood more generally—see many-valued logic). But taken purely syntactically, a rule of inference does not need to preserve any semantic property: any function from sets of formulae to formulae counts as a rule of inference. Usually only rules that are recursive are important; i.e. rules such that there is an effective procedure for determining whether any given formula is the conclusion of a given set of formulae according to the rule. An example of a rule that is not effective in this sense is the infinitary ω-rule.

Popular rules of inference include modus ponens, modus tollens from propositional logic and contraposition. First-order predicate logic uses rules of inference to deal with logical quantifiers. See List of rules of inference for examples.

Overview

In 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

This is just the modus ponens rule 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 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

Main article: Admissible rule

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 $n\,\,\mathsf{nat}$ asserts the fact that $n$ is a natural number):

$\begin{matrix} \frac{}{\mathbf{0} \,\,\mathsf{nat}} & \frac{n \,\,\mathsf{nat}}{\mathbf{s(}n\mathbf{)} \,\,\mathsf{nat}} \\ \end{matrix}$

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:

$\frac{n \,\,\mathsf{nat}}{\mathbf{s(s(}n\mathbf{))} \,\,\mathsf{nat}}$

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:

$\frac{\mathbf{s(}n\mathbf{)} \,\,\mathsf{nat}}{n \,\,\mathsf{nat}}$

This is a true fact of natural numbers, as can be proven by induction. (To prove that this rule is admissible, assume a derivation of the premise and induct on it to produce a derivation of $n\,\,\mathsf{nat}$.) 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:

$\frac{}{\mathbf{s(-3)} \,\,\mathsf{nat}}$

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 $\mathbf{-3} \,\,\mathsf{nat}$. 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 $\vdash$, which means "infers", "proves" or "concludes", (3) a conclusion. This usually embodies the relational (as opposed to functional) view of a rule of inference, where the turnstile stands for a deducibility relation holding between premises and conclusion.

Rules of inference must be distinguished from axioms of a theory. 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. Or, in less technical terms:

Rules are statements ABOUT the system, axioms are statements IN the system. For example:

• The RULE that from $\vdash p$ you can infer $\vdash\text{Provable}(p)$ is a statement that says if you've proven p, then it is provable that p is provable. This holds in Peano arithmetic, for example.
• The Axiom $p \to \text{Provable}(p)$ would mean that every true statement is provable. This does not hold in Peano arithmetic.

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.

See also

• Argument
• Critical thinking
• Deductive reasoning
• Inference objection
• Immediate inference
• Law of thought
• Logical truth