# Definition:Derived Rule

Jump to navigation
Jump to search

## Contents

## Definition

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

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