# Definition:Proof System/Rule of Inference

Jump to navigation
Jump to search

## 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 see

- Definition:Proof Rule, in the context of logic

## 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:

which expresses Modus Ponendo Ponens.

## Sources

- 1959: A.H. Basson and D.J. O'Connor:
*Introduction to Symbolic Logic*(3rd ed.) ... (previous) ... (next): $\S 4.2$: The Construction of an Axiom System - 2012: M. Ben-Ari:
*Mathematical Logic for Computer Science*(3rd ed.) ... (previous) ... (next): $\S 3.1$: Definition $3.1$