# Definition:Sound Proof System

## Definition

Let $\mathcal L$ be a logical language.

Let $\mathscr P$ be a proof system for $\mathcal L$, and let $\mathscr M$ be a formal semantics for $\mathcal L$.

Then $\mathscr P$ is said to be **sound for $\mathscr M$** iff:

Symbolically, this can be expressed as the statement that, for every logical formula $\phi$ of $\mathcal L$:

- $\vdash_{\mathscr P} \phi$ implies $\models_{\mathscr M} \phi$

### Strongly Sound Proof System

$\mathscr P$ is **strongly sound for $\mathscr M$** iff:

- Every $\mathscr P$-provable consequence is an $\mathscr M$-semantic consequence.

Symbolically, this can be expressed as the statement that, for every collection of logical formulas $\mathcal F$, and logical formula $\phi$ of $\mathcal L$:

- $\mathcal F \vdash_{\mathscr P} \phi$ implies $\mathcal F \models_{\mathscr M} \phi$

## Also known as

Many sources obfuscate the distinction between **sound** and **strongly sound**.

Some sources speak of **consistent proof systems**. However, on $\mathsf{Pr} \infty \mathsf{fWiki}$, consistency is a term only applied to (sets of) formulas.

## Also see

## 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 - 1959: A.H. Basson and D.J. O'Connor:
*Introduction to Symbolic Logic*(3rd ed.) ... (previous) ... (next): $\S 4.3$: Derivable Formulae