Rule of inference


Rule of inference

In logic, a rule of inference (also called a transformation rule) is a function from sets of formulae to formulae. The argument is called the "premise set" (or simply "premises") and the value the "conclusion". They can also be viewed as relations holding between premises and conclusions, whereby the conclusion is said to be inferable (or derivable or deducible) from the premises. If the premise set is empty, then the conclusion is said to be a theorem or axiom of the logic.

A desirable property of a rule of inference is that it be "effective" in the sense of e.g. Church 1956. That is, there is an effective procedure for determining whether any given formula is inferable from any given set of formulae. A rule that is not effective is the infinitary omega-rule.

A rule of inference needn't preserve any semantic property such as truth or validity. In fact, there is nothing requiring that a logic characterized purely syntactically have a semantics. A rule may preserve e.g. the property of being the conjunction of the subformula of the longest formula in the premise set.However in many systems rules of inference are used to generate theorems from each other (i.e. to prove theorems).

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. Axiom schemata can also be viewed as rules of inference with zero premises.

Note that there are many different systems of formal logic each one with its own set of well-formed formulas, rules of inference and, sometimes, 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 n,,mathsf{nat} asserts the fact that n is a natural number):

egin{matrix}frac{}{mathbf{0} ,,mathsf{nat &frac{n ,,mathsf{nat{mathbf{s(}nmathbf{)} ,,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(}nmathbf{))} ,,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(}nmathbf{)} ,,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, one would 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 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 o Provable(p) would mean that every true statement is provable. This, however, 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.

ee also

* Inference objection
* Logicism
* List of rules of inference


Wikimedia Foundation. 2010.

Look at other dictionaries:

  • rule of inference — Lewis Carroll raised the Zeno like problem of how a proof ever gets started. Suppose I have as premises (1) p and (2) p →q . Can I infer q ? Only, it seems, if I am sure of (3) (p & p →q ) →q . Can I then infer q ? Only, it seems, if I am sure… …   Philosophy dictionary

  • Inference — is the act or process of deriving a conclusion based solely on what one already knows. Inference is studied within several different fields. * Human inference (i.e. how humans draw conclusions) is traditionally studied within the field of… …   Wikipedia

  • Rule — A rule is:* Rewrite rule, in generative grammar and computer science * Standardization, a formal and widely accepted statement, fact, definition, or qualification * Operation, a determinate rule ( method ) for performing a mathematical operation… …   Wikipedia

  • inference — The process of moving from (possibly provisional) acceptance of some propositions, to acceptance of others. The goal of logic and of classical epistemology is to codify kinds of inference, and to provide principles for separating good from bad… …   Philosophy dictionary

  • inference — in·fer·ence / in fə rəns/ n 1: the act or process of inferring; specif: the act of passing from one proposition, statement, or judgment considered as true to another whose truth is believed to follow logically from that of the former 2: something …   Law dictionary

  • Inference engine — In computer science, and specifically the branches of knowledge engineering and artificial intelligence, an inference engine is a computer program that tries to derive answers from a knowledge base. It is the brain that expert systems use to… …   Wikipedia

  • Rule Interchange Format — Le Rule Interchange Format (RIF ) est une recommandation du W3C. RIF fait partie de la feuille de route du web sémantique, avec principalement SPARQL, RDF et OWL. Bien que prévu initialement par beaucoup comme une couche de règles logiques pour… …   Wikipédia en Français

  • inference on inference, rule of — Means that one presumption or inference may not be based upon another. McManimen v. Public Service Co. of Northern Illinois, 317 Ill.App. 649, 47 N.E.2d 385 …   Black's law dictionary

  • inference on inference, rule of — Means that one presumption or inference may not be based upon another. McManimen v. Public Service Co. of Northern Illinois, 317 Ill.App. 649, 47 N.E.2d 385 …   Black's law dictionary

  • Rule Interchange Format — The Rule Interchange Format (RIF) is a W3C recommendation track effort to develop a format for interchange of rules in rule based systems on the semantic web. The goal is to create an interchange format for different rule languages and inference… …   Wikipedia


Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”

We are using cookies for the best presentation of our site. Continuing to use this site, you agree with this.