Definition:Derived Rule
Jump to navigation
Jump to search
Definition
Let $\LL$ be a formal language.
Let $\mathscr P$ be a proof system for $\LL$.
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 if and only if 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
- Definition:Theorem (Formal Systems), which compares to axioms as derived rules do to rules of inference
Sources
- 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 3.3.2$