Definition:Deduction Rule

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:

• Hilbert Proof System: Instance 1

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

• Rule of Implication

Sources

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