# Definition:Natural Deduction/Proof Rule

It has been suggested that this page or section be merged into Definition:Rule of Inference.also see refactoring on Definition:Natural DeductionTo 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 `{{Mergeto}}` from the code. |

## Definition

A **proof rule** is a rule in natural deduction which allows one to infer the validity of propositional formulas from other propositional formulas.

### Rule of Substitution

Let $S$ be a sequent of propositional logic that has been proved.

Then we may infer any sequent $S'$ resulting from $S$ by substitutions for letters.

### Rule of Sequent Introduction

Let the statements $P_1, P_2, \ldots, P_n$ be conclusions in a proof, on various assumptions.

Let $P_1, P_2, \ldots, P_n \vdash Q$ be a sequent for which we already have a proof.

Then we may infer, at any stage of a proof (citing **SI**), the conclusion $Q$ of the sequent already proved.

This conclusion depends upon the pool of assumptions upon which $P_1, P_2, \ldots, P_n$ rest.

### Rule of Theorem Introduction

We may infer, at any stage of a proof (citing **TI**), a theorem already proved, together with a reference to the theorem that is being cited.

## Structure of a Proof Rule

A proof rule has 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.

## Also known as

Other terms which mean the same thing as **proof rule** when used in the context of logic are:

**rule of derivation****rule of proof****transformation rule****inference rule**or**rule of inference**

However, these may have subtly different meanings when used in different contexts, so when discussing logic, the term **proof rule** is recommended.

## Example

An example of a **proof rule** is:

which expresses Modus Ponendo Ponens.

## Sources

- 1946: Alfred Tarski:
*Introduction to Logic and to the Methodology of Deductive Sciences*(2nd ed.) ... (previous) ... (next): $\S \text{II}.15$: Rules of inference - 1964: Donald Kalish and Richard Montague:
*Logic: Techniques of Formal Reasoning*... (previous) ... (next): $\text{I}$: 'NOT' and 'IF': $\S 3$ - 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 - 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