\begin{definition}[Definition:Semantic Consequence/Predicate Logic]
<section notitle="true" name="tc">
Let $\FF$ be a collection of WFFs of predicate logic.
Then a WFF $\mathbf A$ is a '''semantic consequence''' of $\FF$ {{iff}}:
:$\AA \models_{\mathrm{PL} } \FF$ implies $\AA \models_{\mathrm{PL} } \mathbf A$
for all structures $\AA$, where $\models_{\mathrm{PL} }$ is the models relation.
</section>
\end{definition}