# Definition:Deduction Rule

Jump to navigation
Jump to search

It has been suggested that this page or section be merged into Rule of Implication.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 `{{Mergeto}}` from the code. |

## Theorem

Let $\LL$ be the language of propositional logic.

The **Deduction Rule** is the rule of inference:

- From $U, \mathbf A \vdash \mathbf B$, one may infer $U \vdash \mathbf A \implies \mathbf B$

where:

- $\mathbf A, \mathbf B$ are WFFs of propositional logic
- $U$ is a set of WFFs

For a given proof system, the **Deduction Rule** can be either a basic rule of inference, or a derived rule.

### Applicable Proof Systems

The **Deduction Rule** is either a rule of inference or a derived rule for the following proof systems:

This result is known as the Deduction Theorem.

### Notation

In terms of sequents, the **Deduction Rule** can be denoted as:

- $\dfrac{U, \mathbf A \vdash \mathbf B}{U \vdash \mathbf A \implies \mathbf B}$

## Also see

## Sources

- 2012: M. Ben-Ari:
*Mathematical Logic for Computer Science*(3rd ed.) ... (previous) ... (next): $\S 3.3.2$: Rule $3.13$