Definition:Deduction Rule

From ProofWiki
Jump to navigation Jump to search



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