Definition:Complete Proof System
Jump to navigation
Jump to search
This page is about complete proof system. For other uses, see complete.
Definition
Let $\LL$ be a logical language.
Let $\mathscr P$ be a proof system for $\LL$, and let $\mathscr M$ be a formal semantics for $\LL$.
Then $\mathscr P$ is said to be complete for $\mathscr M$ if and only if:
Symbolically, this can be expressed as the statement that, for every logical formula $\phi$ of $\LL$:
- $\models_{\mathscr M} \phi$ implies $\vdash_{\mathscr P} \phi$
Strongly Complete Proof System
$\mathscr P$ is strongly complete for $\mathscr M$ if and only if:
- Every $\mathscr M$-semantic consequence is a $\mathscr P$-provable consequence.
Symbolically, this can be expressed as the statement that, for every collection $\FF$ of logical formulas, and every logical formula $\phi$ of $\LL$:
- $\FF \models_{\mathscr M} \phi$ implies $\FF \vdash_{\mathscr P} \phi$
Also known as
Many sources obfuscate the distinction between proof systems which are complete and those which are strongly complete.
Also see
- Results about complete proof systems can be found here.
Sources
- 1910: Alfred North Whitehead and Bertrand Russell: Principia Mathematica: Volume $\text { 1 }$ ... (previous) ... (next): Chapter $\text{I}$: Preliminary Explanations of Ideas and Notations
- 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.4$: Conditions for an Axiom System
- 1972: A.G. Howson: A Handbook of Terms used in Algebra and Analysis ... (previous) ... (next): $\S 1$: Some mathematical language: Axiom systems
- 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