# Definition:Theorem/Formal System

Jump to navigation
Jump to search

## Definition

Let $\mathcal L$ be a formal language.

Let $\mathscr P$ be a proof system for $\mathcal L$.

A **theorem of $\mathscr P$** is a well-formed formula of $\mathcal L$ which can be deduced from the axioms and axiom schemata of $\mathscr P$ by means of its rules of inference.

That a WFF $\phi$ is a **theorem** of $\mathscr P$ may be denoted as:

- $\vdash_{\mathscr P} \phi$

## Also known as

A **theorem** $\phi$ of $\mathscr P$ is also called **provable from $\mathscr P$**.

## Also see

- Definition:Theorem of Logic is a specific case of this concept, if one defines the apparatus of logic as a formal system.

## Sources

- 1959: A.H. Basson and D.J. O'Connor:
*Introduction to Symbolic Logic*(3rd ed.) ... (previous) ... (next): $\S 4.3$: Derivable Formulae - 1972: A.G. Howson:
*A Handbook of Terms used in Algebra and Analysis*... (previous) ... (next): $\S 1$: Some mathematical language: Axiom systems - 2012: M. Ben-Ari:
*Mathematical Logic for Computer Science*(3rd ed.) ... (previous): $\S 3.1$: Definition $3.1$