# Definition:Rule of Inference

## Definition

Let $\LL$ be a formal language.

Part of defining a proof system $\mathscr P$ for $\LL$ is to specify its **rules of inference** or **proof rules**.

A **rule of inference** is a specification of a valid means to conclude new theorems in $\mathscr P$ from given theorems and axioms of $\mathscr P$.

Often, the formulation of **rules of inference** also appeals to the notion of provable consequence to be able to deal with assumptions as part of a proof.

## Structure of a Proof Rule

In most cases, an application of a proof rule can be given a **structure**, as follows:

**Definition:**This specifies what the proof rule actually does. Note the careful use of**can**and**may**in the definition:

**Can**implies that it is possible to achieve something based on the structure of the system which is being constructed.**May**implies that this is what this particular proof rule is allowing you to do.

**Abbreviation:**When deriving a sequent, it is convenient to use a precisely defined shorthand to indicate which rule is being applied at a particular point. While important when used in a medium where space is limited, for example in printed books, on $\mathsf{Pr} \infty \mathsf{fWiki}$ these are not so much relied upon.

**Deduced from:**The truth value of a result which is being deduced by a particular proof rule depends on a specific set of premises, or assumptions made during the course of derivation. This pool of assumptions will vary depending on what the proof rule is and what previously derived result or results the proof rule depends on.

**Discharged assumptions:**This specifies which, if any, assumptions have been discharged, that is, no longer contribute to the truth value of the conclusion being derived.

**Depends on:**This specifies the result from which the proof rule*directly*derives its result.

However, some proof systems defy such description, such as the Proof System of Propositional Tableaus.

## Also see

- Definition:Axiom (Formal Systems), the other part in specifying a proof system
- Definition:Derived Rule, which are often convenient in working with a proof system
- Examples of
**proof rules**are gathered in Category:Proof Rules

## Also known as

**Rules of inference** are also known as **rules of transformation** or **transformation rules**.

Further alternatives are **rule of derivation** and **rule of proof**.

With all these, literature might have a specific meaning attached, so be careful before treating any of these as synonyms.

On $\mathsf{Pr} \infty \mathsf{fWiki}$, **proof rule** and **rule of inference** are the terminology of choice and are used interchangeably.

## Example

In the context of propositional logic, an example of a **rule of inference** is:

which expresses Modus Ponendo Ponens.

## Sources

- 1959: A.H. Basson and D.J. O'Connor:
*Introduction to Symbolic Logic*(3rd ed.) ... (previous) ... (next): $\S 4.2$: The Construction of an Axiom System - 1964: Donald Kalish and Richard Montague:
*Logic: Techniques of Formal Reasoning*... (previous) ... (next): $\text{I}$: 'NOT' and 'IF': $\S 3$ - 2000: Michael R.A. Huth and Mark D. Ryan:
*Logic in Computer Science: Modelling and reasoning about systems*... (previous) ... (next): $\S 1.2$: Natural Deduction - 2009: Kenneth Kunen:
*The Foundations of Mathematics*... (previous) ... (next): $\text{II}.10$ Formal Proofs - 2012: M. Ben-Ari:
*Mathematical Logic for Computer Science*(3rd ed.) ... (previous) ... (next): $\S 3.1$: Definition $3.1$

This page may be the result of a refactoring operation.As such, the following source works, along with any process flow, will need to be reviewed. When this has been completed, the citation of that source work (if it is appropriate that it stay on this page) is to be placed above this message, into the usual chronological ordering.In particular: Used to be at what is now Definition:Natural Deduction/Derived Rules. Generic references go here, specific ones to the three derived rules go thereIf you have access to any of these works, then you are invited to review this list, and make any necessary corrections.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{SourceReview}}` from the code. |

- 1946: Alfred Tarski:
*Introduction to Logic and to the Methodology of Deductive Sciences*(2nd ed.) ... (previous) ... (next): $\S \text{II}.15$: Rules of inference - 1965: E.J. Lemmon:
*Beginning Logic*... (previous) ... (next): $\S 1.2$: Conditionals and Negation - 1980: D.J. O'Connor and Betty Powell:
*Elementary Logic*... (previous) ... (next): $\S \text{II}$: The Logic of Statements $(2): \ 1$: Decision procedures and proofs