Definition:Semantic Consequence/Predicate Logic

Definition

Let $\mathcal F$ be a collection of WFFs of predicate logic.

Then a WFF $\mathbf A$ is a semantic consequence of $\mathcal F$ if and only if:

$\mathcal A \models_{\mathrm{PL}} \mathcal F$ implies $\mathcal A \models_{\mathrm{PL}} \mathbf A$

for all structures $\mathcal A$, where $\models_{\mathrm{PL}}$ is the models relation.

Notation

That $\mathbf A$ is a semantic consequence of $\mathcal F$ is denoted as:

$\mathcal F \models_{\mathrm{PL}} \mathbf A$