In the philosophy of logic and logic, specifically in deductive reasoning, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions).
Typically, a rule of inference preserves truth, a semantic property.
But a rule of inference's action is purely syntactic, and does not need to preserve any semantic property: any function from sets of formulae to formulae counts as a rule of inference.
The exact formal language that is used to describe both premises and conclusions depends on the actual context of the derivations.
Rules of inference are often formulated as schemata employing metavariables.
[2] In the rule (schema) above, the metavariables A and B can be instantiated to any element of the universe (or sometimes, by convention, a restricted subset such as propositions) to form an infinite set of inference rules.
In a Hilbert system, the premises and conclusion of the inference rules are simply formulae of some language, usually employing metavariables.
For graphical compactness of the presentation and to emphasize the distinction between axioms and rules of inference, this section uses the sequent notation (
In classical propositional logic, they indeed coincide; the deduction theorem states that A ⊢ B if and only if ⊢ A → B.
There is however a distinction worth emphasizing even in this case: the first notation describes a deduction, that is an activity of passing from sentences to sentences, whereas A → B is simply a formula made with a logical connective, implication in this case.
This point is illustrated in Lewis Carroll's dialogue called "What the Tortoise Said to Achilles",[3] as well as later attempts by Bertrand Russell and Peter Winch to resolve the paradox introduced in the dialogue.
To appreciate the difference, consider the following set of rules for defining the natural numbers (the judgment
In this proof system, the following rule, demonstrating that the second successor of a natural number is also a natural number, is derivable: Its derivation is the composition of two uses of the successor rule above.
However, the rule for finding the predecessor is no longer admissible, because there is no way to derive
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.