# Definition:Deduction Rule

## Theorem

Let $\mathcal L$ 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$