Definition:Deduction Rule

From ProofWiki
Jump to: navigation, search


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$


$\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.


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