Definition:Sound Proof System
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:
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.
Also see
- Results about sound proof systems can be found here.
Linguistic Note
In the context of mathematical logic, the concept sound proof system should be parsed:
- proof system which is sound
and not:
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
- 1998: David Nelson: The Penguin Dictionary of Mathematics (2nd ed.) ... (previous) ... (next): logic
- 2008: David Nelson: The Penguin Dictionary of Mathematics (4th ed.) ... (previous) ... (next): logic