\begin{definition}[Definition:Complete Proof System]
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$''' {{iff}}:
:Every $\mathscr M$-tautology is a $\mathscr P$-theorem.
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$
\end{definition}