Definition:Proof System/Rule of Inference

From ProofWiki
Jump to navigation Jump to search


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 see

Also known as

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


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.