Definition:Derived Rule

From ProofWiki
Jump to: navigation, search


Let $\mathcal L$ be a formal language.

Let $\mathscr P$ be a proof system for $\mathcal L$.

A derived rule for $\mathscr P$ is a rule of inference $R$ such that:

The proof system $\mathscr P'$, obtained by adding $R$ to $\mathscr P$, is equivalent to $\mathscr P$.

That is, $R$ is a derived rule iff it does not extend the collection of $\mathscr P$-theorems.

Also defined as

Some sources make a distinction between derived rules and sound derived rules, where the latter are what are called derived rules on $\mathsf{Pr} \infty \mathsf{fWiki}$.

This distinction is not followed because it is only sensible to call a rule derived if it is actually redundant for the proof system in question.

Also see