# Definition:Sound Proof System

Jump to navigation Jump to search

## Definition

Let $\LL$ be a logical language.

Let $\mathscr P$ be a proof system for $\LL$.

Let $\mathscr M$ be a formal semantics for $\LL$.

Then $\mathscr P$ is said to be sound for $\mathscr M$ if and only if:

Every $\mathscr P$-theorem is an $\mathscr M$-tautology.

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

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

### Strongly Sound Proof System

$\mathscr P$ is strongly sound for $\mathscr M$ if and only if:

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 $\FF$, and logical formula $\phi$ of $\LL$:

$\FF \vdash_{\mathscr P} \phi$ implies $\FF \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.