Definition:Complete Proof System/Strongly Complete

From ProofWiki
Jump to navigation Jump to search


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$.

$\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 $\mathcal F$ of logical formulas, and every logical formula $\phi$ of $\mathcal L$:

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

Also see