# Definition:Proof System/Rule of Inference

## Definition

Let $\mathcal L$ be a formal language.

Part of defining a proof system $\mathscr P$ for $\mathcal L$ is to specify its rules of inference.

A rule of inference is a specification of a valid means to conclude new theorems in $\mathscr P$ from given theorems and axioms of $\mathscr P$.

Often, the formulation of rules of inference also appeals to the notion of provable consequence.

## Also known as

Rules of inference are also known as rules of transformation or transformation rules.

## Example

In the context of propositional logic, an example of a rule of inference is:

If $p$ is a theorem, and $p \implies q$ is a theorem, then $q$ is a theorem.

which expresses Modus Ponendo Ponens.